Wed, 08 Mar 2006 18:37:28 +0100 | wenzelm | infer_derivs: avoid allocating empty MinProof; | changeset | files |
Wed, 08 Mar 2006 18:37:27 +0100 | wenzelm | tuned; | changeset | files |
Wed, 08 Mar 2006 18:37:25 +0100 | wenzelm | Isar/method: goal restriction; | changeset | files |
Wed, 08 Mar 2006 18:37:24 +0100 | wenzelm | constdecl: always allow 'where'; | changeset | files |
Wed, 08 Mar 2006 18:00:00 +0100 | urbanc | deleted some proofs "on comment" | changeset | files |
Wed, 08 Mar 2006 17:55:51 +0100 | urbanc | tuned some proofs | changeset | files |
Wed, 08 Mar 2006 17:54:55 +0100 | urbanc | tuned some of the proofs about fresh_fun | changeset | files |