Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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;
  8. added quickcheck setup
  9. generalized
  10. moved quickcheck setup to distribution
  11. moved generic instance to distribution
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 (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70908:3828a57e537d by wenzelm:
tuned signature;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70907:7e3f25a0cee4 by wenzelm:
proper protocol_message for bootstrap proofs;
The file was modified src/Pure/General/output.ML (diff)
The file was modified src/Pure/PIDE/protocol_message.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 70906:b9567a9f44a0 by wenzelm:
proper export of bootstrap proofs (amending a6304b4664b6);
The file was modified src/Pure/ROOT (diff)
Changeset 70905:a6304b4664b6 by wenzelm:
more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;
The file was modified src/Pure/ROOT (diff)
Changeset 70904:caf91f9b847b by wenzelm:
proper treatment of self thm_id;<br>clarified signature;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
Changeset 70903:c550368a4e29 by haftmann:
added quickcheck setup
The file was modified src/HOL/ex/Word_Type.thy (diff)
Changeset 70902:cb161182ce7f by haftmann:
generalized
The file was modified src/HOL/Rings.thy (diff)
Changeset 70901:94a0c47b8553 by haftmann:
moved quickcheck setup to distribution
The file was modified src/HOL/Library/Type_Length.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 70900:954e7f79c25a by haftmann:
moved generic instance to distribution
The file was modified src/HOL/Word/Word.thy (diff)