Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- misc tuning and clarification: more standard Same.commit discipline;
- tuned;
- tuned names;
- more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term;
- minor performance tuning: more careful treatment of empty environment;
- clarified signature;
- more zproofs;
- clarified signature: support shared cache;
- tuned;
- tuned: avoid shadowing;
- more zproofs;
- tuned;
- more operations; clarified cache;
- tuned signature;
- tuned names;
- tuned -- eliminate clones;
- tuned;
- more operations;
- more operations;
- tuned;
- clarified signature;
- tuned;
- tuned;
- consider schedule calculation time in estimation;
- compare previous build schedule with new one, to prevent regressions;
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/logic.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/envir.ML |
The file was modified | src/Pure/thm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/thm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/thm.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/thm.ML |
The file was modified | src/Pure/thm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/term.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/term_items.ML |
The file was modified | src/Pure/term.ML |
The file was modified | src/HOL/Tools/datatype_realizer.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/term.ML |
The file was modified | src/Pure/envir.ML |
The file was modified | src/Pure/Tools/build_schedule.scala |
The file was modified | src/Pure/Tools/build_schedule.scala |