Summary
- tuned;
- clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp);
- clarified box_proof: use sort constraints within the logic;
- more operations (see also 8368160d3c65);
The file was modified | src/Pure/zterm.ML (diff) |
The file was modified | src/Pure/zterm.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) |