Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. tuned signature: more exports;
  3. clarified signature: prefer internal Thm_Name.T over external Facts.ref;
  4. more robust / permissive;
  5. clarified signature: more operations;
  6. tuned;
  7. clarified operations, following pretty_thm_name;
  8. more accurate treatment of Thm_Name.T;
Changeset 80332:4bed658a01fc by wenzelm:
merged
Changeset 80331:6f25a035069c by wenzelm:
tuned signature: more exports;
The file was modified src/Pure/Tools/find_theorems.ML
Changeset 80330:e01aae620437 by wenzelm:
clarified signature: prefer internal Thm_Name.T over external Facts.ref;
The file was modified src/Pure/Tools/find_theorems.ML
The file was modified src/Pure/thm_name.ML
Changeset 80329:d90a96894644 by wenzelm:
more robust / permissive;
The file was modified src/Pure/Isar/proof_context.ML
Changeset 80328:559909bd7715 by wenzelm:
clarified signature: more operations;
The file was modified src/HOL/Library/code_test.ML
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML
The file was modified src/HOL/Tools/Nitpick/nitpick.ML
The file was modified src/Pure/General/pretty.ML
The file was modified src/Pure/Isar/proof_context.ML
The file was modified src/Pure/Isar/proof_display.ML
The file was modified src/Pure/Tools/find_theorems.ML
The file was modified src/Pure/unify.ML
The file was modified src/Tools/Code/code_target.ML
Changeset 80327:e4e643705d90 by wenzelm:
tuned;
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
Changeset 80326:53f12ab896e6 by wenzelm:
clarified operations, following pretty_thm_name;
The file was modified src/Pure/Isar/proof_context.ML
Changeset 80325:dca37c6479e3 by wenzelm:
more accurate treatment of Thm_Name.T;
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML