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

- 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;

Thm.proof_of returns proof_body;
adapted PThm;

refined notion of derivation, consiting of promises and proof_body;
removed oracle_of (would require detailed check wrt. promises);
proof_of returns proof_body;