Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;
- support dummy term;
- tuned signature;
- proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
- proper Thm.transfer;
- clarified files;
- clarified proof_boxes (requires prune_proofs=false);
- tuned;
- more robust;
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/term.scala |
The file was modified | src/Pure/Thy/export_theory.ML |
The file was modified | src/Pure/Thy/export_theory.scala |
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 |
The file was modified | src/Pure/global_theory.ML |
The file was added | src/Pure/thm_deps.ML |
The file was modified | src/Pure/ROOT.ML |
The file was removed | src/Pure/Thy/thm_deps.ML |
The file was modified | src/Pure/Thy/export_theory.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/Thy/export_theory.scala |
The file was modified | src/Pure/Thy/export_theory.scala |