Summary
- discontinued ASCII syntax;
- global declaration of abstract syntax for proof terms, with qualified names; clarified modules;
- tuned;
- tuned;
The file was modified | src/Doc/Implementation/Logic.thy (diff) |
The file was modified | src/Pure/Proof/proof_syntax.ML (diff) |
The file was modified | src/HOL/Tools/rewrite_hol_proof.ML (diff) |
The file was modified | src/Pure/Proof/proof_syntax.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/pure_thy.ML (diff) |
The file was modified | src/Pure/pure_thy.scala (diff) |
The file was modified | src/HOL/Tools/SMT/smt_builtin.ML (diff) |
The file was modified | src/Pure/Isar/class.ML (diff) |
The file was modified | src/Pure/Isar/class_declaration.ML (diff) |
The file was modified | src/Pure/Isar/object_logic.ML (diff) |
The file was modified | src/Pure/Proof/proof_syntax.ML (diff) |
The file was modified | src/Pure/axclass.ML (diff) |
The file was modified | src/Tools/Code/code_runtime.ML (diff) |
The file was modified | src/Pure/Thy/export_theory.ML (diff) |