Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- tuned signature: more exports;
- clarified signature: prefer internal Thm_Name.T over external Facts.ref;
- more robust / permissive;
- clarified signature: more operations;
- tuned;
- clarified operations, following pretty_thm_name;
- more accurate treatment of Thm_Name.T;
The file was modified | src/Pure/Tools/find_theorems.ML |
The file was modified | src/Pure/Tools/find_theorems.ML |
The file was modified | src/Pure/thm_name.ML |
The file was modified | src/Pure/Isar/proof_context.ML |
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 |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML |
The file was modified | src/Pure/Isar/proof_context.ML |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML |