Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
  2. clarified signature;
  3. tuned;
  4. more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;
  5. clarified signature;
  6. observe option "prune_proofs";
Changeset 79336:032a31db4c6f by wenzelm:
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
The file was modified src/HOL/HOLCF/Tools/Domain/domain_constructors.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_induction.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML (diff)
The file was modified src/HOL/HOLCF/ex/Pattern_Match.thy (diff)
The file was modified src/HOL/Import/import_rule.ML (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Nominal/nominal_atoms.ML (diff)
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_rep_datatype.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML (diff)
The file was modified src/HOL/Tools/choice_specification.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Types_To_Sets/unoverload_def.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/axclass.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/ZF/Tools/datatype_package.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
The file was modified src/ZF/Tools/primrec_package.ML (diff)
Changeset 79335:6d167422bcb0 by wenzelm:
clarified signature;
The file was modified src/Pure/thm.ML (diff)
Changeset 79334:afd26cc61e8d by wenzelm:
tuned;
The file was modified src/Pure/global_theory.ML (diff)
Changeset 79333:56b604882d0b by wenzelm:
more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79332:40cabd57aac3 by wenzelm:
clarified signature;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 79331:8e0c80a9beb6 by wenzelm:
observe option "prune_proofs";
The file was modified src/Pure/thm.ML (diff)