Summary
- more operations: zterm ordering that follows fast_term_ord;
- clarified signature; clarified modules;
- clarified modules;
- more zproofs;
- more zproofs, imitating existing proofs (which are a bit rough here);
- tuned signature;
- tuned whitespace;
- minor performance tuning;
The file was modified | src/Pure/zterm.ML (diff) |
The file was modified | src/Pure/Proof/extraction.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) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/Pure/zterm.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/Pure/zterm.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |