Skip to content
Success

Changes

Summary

  1. discontinued ASCII syntax;
  2. global declaration of abstract syntax for proof terms, with qualified names; clarified modules;
  3. tuned;
  4. tuned;
Changeset 70389:2adff54de67e by wenzelm:
discontinued ASCII syntax;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
Changeset 70388:e31271559de8 by wenzelm:
global declaration of abstract syntax for proof terms, with qualified names;<br>clarified modules;
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)
Changeset 70387:35dd9212bf29 by wenzelm:
tuned;
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)
Changeset 70386:6af87375b95f by wenzelm:
tuned;
The file was modified src/Pure/Thy/export_theory.ML (diff)