berghofe [Sun, 16 Nov 2008 18:19:27 +0100] rev 28813
- Corrected order of quantification over Frees.
- Fixed bug in handling of TFrees that caused variable order to get mixed up.
berghofe [Sun, 16 Nov 2008 18:18:45 +0100] rev 28812
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.
wenzelm [Sat, 15 Nov 2008 21:31:37 +0100] rev 28811
adapted PThm and MinProof;
wenzelm [Sat, 15 Nov 2008 21:31:36 +0100] rev 28810
retrieve thm deps from proof_body;
removed obsolete enable/disable operation;
wenzelm [Sat, 15 Nov 2008 21:31:35 +0100] rev 28809
retrieve thm deps from proof_body;
wenzelm [Sat, 15 Nov 2008 21:31:32 +0100] rev 28808
adapted PThm;
wenzelm [Sat, 15 Nov 2008 21:31:30 +0100] rev 28807
proof_of_term: removed obsolete disambiguisation table;
adapted PThm;
Thm.proof_of returns proof_body;
wenzelm [Sat, 15 Nov 2008 21:31:29 +0100] rev 28806
rewrite_proof: simplified simprocs (no name required);
adapted PThm;
fold_proof_atoms;
wenzelm [Sat, 15 Nov 2008 21:31:27 +0100] rev 28805
Thm.proof_of returns proof_body;
adapted PThm;
wenzelm [Sat, 15 Nov 2008 21:31:25 +0100] rev 28804
refined notion of derivation, consiting of promises and proof_body;
removed oracle_of (would require detailed check wrt. promises);
proof_of returns proof_body;