Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid spurious shyps (with vacous type variable);
  2. merged
  3. more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
  4. clarified signature: name of standard_proof is authentic, otherwise empty;
  5. clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;
  6. option to export standardized proof terms (not scalable);
  7. more kinds, notably for Isabelle/MMT;
  8. refined proof of concept for bit operations
  9. more lemmas
Changeset 70919:692095bafcd9 by wenzelm:
avoid spurious shyps (with vacous type variable);
The file was modified src/Pure/Thy/export_theory.ML (diff)
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 (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 70916:4c15217d6266 by wenzelm:
clarified signature: name of standard_proof is authentic, otherwise empty;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/term.scala (diff)
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 (diff)
The file was modified src/HOL/Proofs/ex/XML_Data.thy (diff)
The file was modified src/HOL/Tools/inductive_realizer.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Proof/proof_rewrite_rules.ML (diff)
The file was modified src/Pure/Proof/proof_syntax.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/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70914:05c4c6a99b3f by wenzelm:
option to export standardized proof terms (not scalable);
The file was modified etc/options (diff)
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 (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
Changeset 70913:935c78a90ee0 by wenzelm:
more kinds, notably for Isabelle/MMT;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 70912:8c2bef3df488 by haftmann:
refined proof of concept for bit operations
The file was modified src/HOL/ex/Bit_Lists.thy (diff)
Changeset 70911:38298c04c12e by haftmann:
more lemmas
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Parity.thy (diff)