Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- tuned structure;
- tuned;
- merged
- performance tuning: cache for ztyp_of within zterm_of; clarified signature;
- tuned names;
- minor performance tuning;
- more zproofs;
- minor performance tuning;
- tuned;
- more zproofs;
- clarified modules;
- more zproofs;
- more zproofs;
- proper treatment of ZConstP: term represents body of closure;
- proper substitution of types within term;
- more accurate treatment of term variables after instantiation of type variables;
- tuned signature;
- tuned;
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.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/zterm.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/zterm.ML |
The file was modified | src/Pure/proofterm.ML |
The file was modified | src/Pure/type.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/zterm.ML |
The file was modified | src/Pure/term_items.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.ML |
The file was modified | src/Pure/zterm.ML |