Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified proof_body: cover zboxes from zproof;
  3. pro-forma support for optional zproof: no proper content yet;
  4. clarified signature: follow Term.could_unify;
  5. clarified bootstrap --- modules related to proofterm.ML;
Changeset 79115:0c7de2ae814b by wenzelm:
merged
Changeset 79114:686b7b14d041 by wenzelm:
clarified proof_body: cover zboxes from zproof;
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/zterm.ML (diff)
Changeset 79113:5109e4b2a292 by wenzelm:
pro-forma support for optional zproof: no proper content yet;
The file was modified src/HOL/Tools/datatype_realizer.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/zterm.ML (diff)
Changeset 79112:fd9de06c0ecf by wenzelm:
clarified signature: follow Term.could_unify;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79111:8fb4013f2ac2 by wenzelm:
clarified bootstrap --- modules related to proofterm.ML;
The file was modified src/Pure/ROOT.ML (diff)