Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. merged
  2. export toplevel proof similar to named PThm;
  3. tuned signature;
  4. proper protocol_message for bootstrap proofs;
  5. proper export of bootstrap proofs (amending a6304b4664b6);
  6. more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;
  7. proper treatment of self thm_id; clarified signature;
Changeset 70910:3ed399935d7c by wenzelm:
merged
Changeset 70909:9e05f382e749 by wenzelm:
export toplevel proof similar to named PThm;
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/proofterm.ML
Changeset 70908:3828a57e537d by wenzelm:
tuned signature;
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/thm.ML
Changeset 70907:7e3f25a0cee4 by wenzelm:
proper protocol_message for bootstrap proofs;
The file was modified src/Pure/General/output.ML
The file was modified src/Pure/PIDE/protocol_message.ML
The file was modified src/Pure/ROOT.ML
The file was modified src/Pure/Thy/export.ML
The file was modified src/Pure/Tools/build.ML
Changeset 70906:b9567a9f44a0 by wenzelm:
proper export of bootstrap proofs (amending a6304b4664b6);
The file was modified src/Pure/ROOT
Changeset 70905:a6304b4664b6 by wenzelm:
more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;
The file was modified src/Pure/ROOT
Changeset 70904:caf91f9b847b by wenzelm:
proper treatment of self thm_id;<br>clarified signature;
The file was modified src/Pure/Thy/export_theory.ML
The file was modified src/Pure/global_theory.ML