Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

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

Summary

  1. merged
  2. more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
  3. clarified signature: name of standard_proof is authentic, otherwise empty;
  4. clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;
  5. option to export standardized proof terms (not scalable);
  6. more kinds, notably for Isabelle/MMT;
Changeset 70918:d36f600c6500 by wenzelm:
merged
Changeset 70917:693e811b91bb by wenzelm:
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
The file was modified src/Pure/ROOT
The file was modified src/Pure/Thy/export_theory.ML
Changeset 70916:4c15217d6266 by wenzelm:
clarified signature: name of standard_proof is authentic, otherwise empty;
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/term.scala
Changeset 70915:bd4d37edfee4 by wenzelm:
clarified expand_proof/expand_name: allow more detailed control via thm_header;<br>export_standard_proofs: authentic theorem names in &quot;print&quot; format;
The file was modified src/Doc/Implementation/Logic.thy
The file was modified src/HOL/Proofs/ex/XML_Data.thy
The file was modified src/HOL/Tools/inductive_realizer.ML
The file was modified src/Pure/Proof/extraction.ML
The file was modified src/Pure/Proof/proof_rewrite_rules.ML
The file was modified src/Pure/Proof/proof_syntax.ML
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/more_thm.ML
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/thm.ML
Changeset 70914:05c4c6a99b3f by wenzelm:
option to export standardized proof terms (not scalable);
The file was modified etc/options
The file was modified src/HOL/Proofs/ex/XML_Data.thy
The file was modified src/Pure/Proof/proof_syntax.ML
The file was modified src/Pure/ROOT
The file was modified src/Pure/System/isabelle_process.ML
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/more_thm.ML
Changeset 70913:935c78a90ee0 by wenzelm:
more kinds, notably for Isabelle/MMT;
The file was modified src/Pure/Thy/export_theory.scala