Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
  3. clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
  4. refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
  5. tuned;
  6. more uniform schedule_theories, notably for "present" and "commit" phase after loading;
  7. tuned;
  8. moved more legacy to AFP
Changeset 73823:c10fe904ac10 by wenzelm:
merged
Changeset 73822:1192c68ebe1c by wenzelm:
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 73821:9ead8d9be3ab by wenzelm:
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
The file was modified etc/options (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 73820:745e2cd1f5f5 by wenzelm:
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
Changeset 73819:60214976d846 by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 73818:d67688992bde by wenzelm:
more uniform schedule_theories, notably for "present" and "commit" phase after loading;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 73817:df0fd744e6bb by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 73816:0510c7a4256a by haftmann:
moved more legacy to AFP
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Library/Word.thy (diff)