Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. proper inst table;
  3. more scalable data structure (but: rarely used many arguments);
  4. minor performance tuning: fewer allocations; clarified theory context;
Changeset 74222:bf595bfbdc98 by wenzelm:
tuned;
The file was modified src/Pure/term_subst.ML (diff)
Changeset 74221:291e71ed0174 by wenzelm:
proper inst table;
The file was modified src/HOL/Eisbach/match_method.ML (diff)
Changeset 74220:c49134ee16c1 by wenzelm:
more scalable data structure (but: rarely used many arguments);
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/subgoal.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/consts.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/morphism.ML (diff)
The file was modified src/Pure/proofterm.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)
The file was modified src/Pure/variable.ML (diff)
Changeset 74219:1d25be2353e1 by wenzelm:
minor performance tuning: fewer allocations;<br>clarified theory context;
The file was modified src/Pure/thm.ML (diff)