Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. tuned;
  3. proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
  4. revert temporary workaround 6d111935299c;
  5. added lemma
Changeset 74748:95643a0bff49 by wenzelm:
tuned;
The file was modified src/Pure/Thy/latex.scala (diff)
Changeset 74747:10991d115fff by wenzelm:
tuned;
The file was modified src/Pure/Thy/document_build.scala (diff)
Changeset 74746:56fe200b7121 by wenzelm:
proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala (diff)
Changeset 74745:f54c81fe84f2 by wenzelm:
revert temporary workaround 6d111935299c;
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
Changeset 74744:ed1e5ea25369 by nipkow:
added lemma
The file was modified src/HOL/List.thy (diff)