summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

proof_body/pthm: removed redundant types field;
fold_proof_atoms: unified recursive case with fold_body_thms;
tuned signature;

clarified Thm.proof_body_of vs. Thm.proof_of;

- Corrected order of quantification over Frees.
- Fixed bug in handling of TFrees that caused variable order to get mixed up.

Frees in PThms are now quantified in the order of their appearance in the
proposition as well, to make it compatible (again) with variable order used
by forall_intr_frees.

adapted PThm and MinProof;

retrieve thm deps from proof_body;
removed obsolete enable/disable operation;

retrieve thm deps from proof_body;

adapted PThm;

proof_of_term: removed obsolete disambiguisation table;
adapted PThm;
Thm.proof_of returns proof_body;

rewrite_proof: simplified simprocs (no name required);
adapted PThm;
fold_proof_atoms;