Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned comments;
  2. merged
  3. retain type information from reconstruct_proof, notably for Export_Theory.export_thm;
  4. tuned proofs;
  5. clarified modules;
  6. more robust;
  7. tuned modules;
  8. tuned proofs -- more stable proof terms without [rule_format];
  9. merged
  10. A slight tidying up of messy proof steps
Changeset 71092:3c04a52c422a by wenzelm:
tuned comments;
The file was modified src/HOL/Tools/rewrite_hol_proof.ML (diff)
Changeset 71091:fd82d53c1761 by wenzelm:
merged
Changeset 71090:06c6495fb1d0 by wenzelm:
retain type information from reconstruct_proof, notably for Export_Theory.export_thm;
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
Changeset 71089:907b7a6471a0 by wenzelm:
tuned proofs;
The file was modified src/ZF/List.thy (diff)
Changeset 71088:4b45d592ce29 by wenzelm:
clarified modules;
The file was modified src/HOL/Proofs/ex/XML_Data.thy (diff)
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 71087:77580c977e0c by wenzelm:
more robust;
The file was modified src/Pure/Proof/proof_rewrite_rules.ML (diff)
Changeset 71086:aedd11603fb4 by wenzelm:
tuned modules;
The file was modified src/Pure/ROOT.ML (diff)
Changeset 71085:950e1cfe0fe4 by wenzelm:
tuned proofs -- more stable proof terms without [rule_format];
The file was modified src/ZF/Nat.thy (diff)
The file was modified src/ZF/Ordinal.thy (diff)
The file was modified src/ZF/WF.thy (diff)
The file was modified src/ZF/equalities.thy (diff)
The file was modified src/ZF/func.thy (diff)
Changeset 71084:c4458eb355c0 by paulson:
merged
Changeset 71083:ce92360f0692 by paulson _lp15@cam.ac.uk_:
A slight tidying up of messy proof steps
The file was modified src/HOL/Library/Ramsey.thy (diff)