| Sat, 15 Nov 2008 21:31:32 +0100 | wenzelm | adapted PThm; | changeset | files |
| Sat, 15 Nov 2008 21:31:30 +0100 | wenzelm | proof_of_term: removed obsolete disambiguisation table; | changeset | files |
| Sat, 15 Nov 2008 21:31:29 +0100 | wenzelm | rewrite_proof: simplified simprocs (no name required); | changeset | files |
| Sat, 15 Nov 2008 21:31:27 +0100 | wenzelm | Thm.proof_of returns proof_body; | changeset | files |
| Sat, 15 Nov 2008 21:31:25 +0100 | wenzelm | refined notion of derivation, consiting of promises and proof_body; | changeset | files |
| Sat, 15 Nov 2008 21:31:23 +0100 | wenzelm | reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); | changeset | files |
| Sat, 15 Nov 2008 21:31:21 +0100 | wenzelm | pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises); | changeset | files |
| Sat, 15 Nov 2008 21:31:20 +0100 | wenzelm | ProofSyntax.proof_of_term: removed obsolete disambiguisation table; | changeset | files |