Skip to content
Success

Changes

Summary

  1. tuned comments -- proper sections;
  2. support export_proofs, prune_proofs; tuned comments;
  3. clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
  4. tuned;
  5. clarified exception;
  6. tuned;
  7. more accurate type information;
  8. unused (see also 42fbb6abed5a);
Changeset 70397:f5bce5af361b by wenzelm:
tuned comments -- proper sections;
The file was modified src/Pure/Proof/reconstruct.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70396:425c5f9bc61a by wenzelm:
support export_proofs, prune_proofs;<br>tuned comments;
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)
Changeset 70395:af88c05696bd by wenzelm:
clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70394:893d6373b484 by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70393:9e53a98702b9 by wenzelm:
clarified exception;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70392:59f16c087840 by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70391:47fd6c7b9559 by wenzelm:
more accurate type information;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70390:772321761cb8 by wenzelm:
unused (see also 42fbb6abed5a);
The file was modified src/Pure/Proof/proof_syntax.ML (diff)