Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;
  2. support dummy term;
  3. tuned signature;
  4. proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
  5. proper Thm.transfer;
  6. clarified files;
  7. clarified proof_boxes (requires prune_proofs=false);
  8. tuned;
  9. more robust;
Changeset 70898:c13d9d3ee128 by wenzelm:
turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;
The file was modified src/Pure/proofterm.ML
Changeset 70897:2cc7c05b3b3c by wenzelm:
support dummy term;
The file was modified src/Pure/term.scala
Changeset 70896:8017d382a0d7 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/Thy/export_theory.scala
Changeset 70895:2a318149b01b by wenzelm:
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/thm_deps.ML
Changeset 70894:15adbeb1fabd by wenzelm:
proper Thm.transfer;
The file was modified src/Pure/global_theory.ML
Changeset 70893:ce1e27dcc9f4 by wenzelm:
clarified files;
The file was addedsrc/Pure/thm_deps.ML
The file was modified src/Pure/ROOT.ML
The file was removedsrc/Pure/Thy/thm_deps.ML
Changeset 70892:aadb5c23af24 by wenzelm:
clarified proof_boxes (requires prune_proofs=false);
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/proofterm.ML
Changeset 70891:f21a76a4d01f by wenzelm:
tuned;
The file was modified src/Pure/Thy/export_theory.scala
Changeset 70890:15ad4c045590 by wenzelm:
more robust;
The file was modified src/Pure/Thy/export_theory.scala