| Wed, 25 Mar 2009 21:35:49 +0100 | wenzelm | @{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism; | changeset | files |
| Wed, 25 Mar 2009 21:34:31 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 25 Mar 2009 17:23:44 +0100 | wenzelm | use more informative Thm.proof_body_of for oracle demo; | changeset | files |
| Wed, 25 Mar 2009 16:54:49 +0100 | wenzelm | Proofterm.approximate_proof_body; | changeset | files |
| Wed, 25 Mar 2009 16:54:17 +0100 | wenzelm | fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete); | changeset | files |
| Wed, 25 Mar 2009 16:52:50 +0100 | wenzelm | removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof; | changeset | files |