Summary
- tuned comments -- proper sections;
- support export_proofs, prune_proofs; tuned comments;
- clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
- tuned;
- clarified exception;
- tuned;
- more accurate type information;
- unused (see also 42fbb6abed5a);
The file was modified | src/Pure/Proof/reconstruct.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | etc/options (diff) |
The file was modified | src/Pure/ROOT.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
The file was modified | src/Pure/Proof/proof_syntax.ML (diff) |