Skip to content
Success

Changes

Summary

  1. actually use theory;
  2. clarified parent session images, to avoid duplicate loading of theories;
  3. merged
  4. tuned documentation;
  5. support for potential session imports;
  6. more checks;
  7. tuned messages;
  8. actually use theory; tuned;
  9. renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
  10. support for Mercurial manifest check;
  11. tuned;
  12. more operations;
  13. support for multiple operations via options;
  14. clarified tool name -- more official status;
  15. more lemmas
  16. include GCD as integral part of computational algebra in session HOL
  17. prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);
  18. added missing file (amending f533820e7248);
Changeset 65570:660df4a6dc59 by wenzelm:
actually use theory;
The file was modified src/HOL/ROOT (diff)
Changeset 65569:3cb6f3281ef1 by wenzelm:
clarified parent session images, to avoid duplicate loading of theories;
The file was modified src/Doc/ROOT (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/ZF/ROOT (diff)
Changeset 65568:1070be576372 by wenzelm:
merged
Changeset 65567:c556c09765dd by wenzelm:
tuned documentation;
The file was modified Admin/Release/CHECKLIST (diff)
The file was modified NEWS (diff)
Changeset 65566:94c514ea2846 by wenzelm:
support for potential session imports;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 65565:3219a7ed669c by wenzelm:
more checks;
The file was modified Admin/Release/CHECKLIST (diff)
Changeset 65564:5b3cae328a94 by wenzelm:
tuned messages;
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 65563:e83c9e94e891 by wenzelm:
actually use theory;<br>tuned;
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/ex/Case_Product.thy (diff)
Changeset 65562:f9753d949afc by wenzelm:
renamed theory to avoid conflict with loaded theory &quot;Tree&quot; from HOL-Library;
The file was addedsrc/HOL/Induct/Infinitely_Branching_Tree.thy
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Induct/Tree.thy
Changeset 65561:741b1d3930c0 by wenzelm:
support for Mercurial manifest check;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 65560:327842649e8d by wenzelm:
tuned;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 65559:7ff7781913a4 by wenzelm:
more operations;
The file was modified src/Pure/General/mercurial.scala (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 65558:479406635409 by wenzelm:
support for multiple operations via options;
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 65557:29c69a599743 by wenzelm:
clarified tool name -- more official status;
The file was addedsrc/Pure/Tools/imports.scala
The file was modified NEWS (diff)
The file was modified src/Pure/System/isabelle_tool.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was removedsrc/Pure/Tools/update_imports.scala
Changeset 65556:fcd599570afa by haftmann:
more lemmas
The file was modified src/HOL/Divides.thy (diff)
Changeset 65555:85ed070017b7 by haftmann:
include GCD as integral part of computational algebra in session HOL
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Nitpick.thy (diff)
Changeset 65554:a04afc400156 by wenzelm:
prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 65553:006a274cdbc2 by wenzelm:
added missing file (amending f533820e7248);
The file was addedsrc/HOL/Main.thy