Skip to content
Success

Changes

Summary

  1. minor performance tuning: proper Same.operation;
  2. minor performance tuning: proper Same.operation; clarified modules;
  3. tuned signature;
  4. minor performance tuning: proper Same.operation; clarified modules;
  5. minor performance tuning: proper Same.operation;
  6. tuned signature;
  7. tuned;
  8. pro-forma support for ZTerm.sorts_zproof;
  9. tuned comments;
  10. tuned structure;
  11. minor performance tuning: proper Same.operation;
  12. tuned names (again);
Changeset 79412:1c758cd8d5b2 by wenzelm:
minor performance tuning: proper Same.operation;
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML (diff)
The file was modified src/HOL/Tools/choice_specification.ML (diff)
The file was modified src/HOL/Types_To_Sets/unoverload_type.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/type.ML (diff)
Changeset 79411:700d4f16b5f2 by wenzelm:
minor performance tuning: proper Same.operation;<br>clarified modules;
The file was modified src/HOL/Tools/inductive_realizer.ML (diff)
The file was modified src/Pure/Isar/class.ML (diff)
The file was modified src/Pure/Isar/class_declaration.ML (diff)
The file was modified src/Pure/Isar/code.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/Thy/export_theory.ML (diff)
The file was modified src/Pure/axclass.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/term.ML (diff)
The file was modified src/Pure/type.ML (diff)
The file was modified src/Pure/type_infer_context.ML (diff)
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 79410:719563e4816a by wenzelm:
tuned signature;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 79409:e1895596e1b9 by wenzelm:
minor performance tuning: proper Same.operation;<br>clarified modules;
The file was modified src/HOL/Tools/SMT/z3_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/envir.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/term.ML (diff)
The file was modified src/Pure/term_subst.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/type_infer.ML (diff)
Changeset 79408:d9cf62ea273d by wenzelm:
minor performance tuning: proper Same.operation;
The file was modified src/Pure/logic.ML (diff)
Changeset 79407:c6c2e41cac1c by wenzelm:
tuned signature;
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79406:826a1ae59cac by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79405:f4fdf5eebcac by wenzelm:
pro-forma support for ZTerm.sorts_zproof;
The file was modified src/Pure/Proof/proof_rewrite_rules.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/zterm.ML (diff)
Changeset 79404:cb19148c0b95 by wenzelm:
tuned comments;
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 79403:254b062ec54d by wenzelm:
tuned structure;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79402:6bcb7131142d by wenzelm:
minor performance tuning: proper Same.operation;
The file was modified src/Pure/thm.ML (diff)
Changeset 79401:6e6f76c5dd96 by wenzelm:
tuned names (again);
The file was modified src/Pure/thm.ML (diff)