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

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;

reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
added type proof_body, which covers oracles and thms of local proof;
added general fold_body_thms, fold_proof_atoms;
removed thms_of_proof, thms_of_proof', axms_of_proof;
slightly more abstract handling of body content (oracles, thms);
rewrite_proof: simplified simprocs (no name required);
thm_proof: lazy fulfillment of promises;