Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more support for proof terms; clarified signature;
  2. more support for proof terms;
  3. support for proof terms;
  4. clarified proof export;
  5. set_preproc for object-logics with type classes;
  6. tuned signature;
  7. skip (somewhat pointless) shrink_proof more uniformly;
  8. apply_preproc for all proof boxes;
  9. cumulative errors for session partitions;
  10. proper guard for process_theory: ensure uniform precedence of results;
  11. load HOL-Proofs first: it introduces some extra "thm" items that are required later on;
Changeset 70884:84145953b2a5 by wenzelm:
more support for proof terms;<br>clarified signature;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70883:93767b7a8e7b by wenzelm:
more support for proof terms;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 70882:dbc82c54f6f0 by wenzelm:
support for proof terms;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 70881:80f3a290b35c by wenzelm:
clarified proof export;
The file was modified src/Pure/Thy/export_theory.scala (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70880:de2e2382bc0d by wenzelm:
set_preproc for object-logics with type classes;
The file was modified src/FOL/IFOL.thy (diff)
The file was modified src/FOLP/IFOLP.thy (diff)
The file was modified src/Sequents/LK0.thy (diff)
Changeset 70879:0b320e92485c by wenzelm:
tuned signature;
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/Pure/Proof/proof_rewrite_rules.ML (diff)
Changeset 70878:69050518d4f3 by wenzelm:
skip (somewhat pointless) shrink_proof more uniformly;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70877:f2ce687bfa0a by wenzelm:
apply_preproc for all proof boxes;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70876:91b311e7d040 by wenzelm:
cumulative errors for session partitions;
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/update.scala (diff)
Changeset 70875:a62c34770df9 by wenzelm:
proper guard for process_theory: ensure uniform precedence of results;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 70874:2010397f7c9a by wenzelm:
load HOL-Proofs first: it introduces some extra &quot;thm&quot; items that are required later on;
The file was modified src/Pure/Tools/dump.scala (diff)