| Sat, 26 Nov 2005 18:41:41 +0100 | berghofe | Corrected treatment of non-recursive abstraction types. | changeset | files |
| Fri, 25 Nov 2005 21:14:34 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Fri, 25 Nov 2005 20:57:51 +0100 | wenzelm | induct: insert defs in object-logic form; | changeset | files |
| Fri, 25 Nov 2005 19:20:56 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Fri, 25 Nov 2005 19:09:44 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Fri, 25 Nov 2005 18:58:43 +0100 | wenzelm | consume: unfold defs in all major prems; | changeset | files |
| Fri, 25 Nov 2005 18:58:42 +0100 | wenzelm | revert_skolem: fall back on Syntax.deskolem; | changeset | files |