| Thu, 26 Mar 2009 14:14:02 +0100 | wenzelm | simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy; | changeset | files |
| 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 |