| 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 |
| Fri, 25 Nov 2005 18:58:41 +0100 | wenzelm | forall_conv ~1; | changeset | files |
| Fri, 25 Nov 2005 18:58:40 +0100 | wenzelm | added dummy_pattern; | changeset | files |
| Fri, 25 Nov 2005 18:58:38 +0100 | wenzelm | tuned names; | changeset | files |
| Fri, 25 Nov 2005 18:58:37 +0100 | wenzelm | forall_conv: limit prefix; | changeset | files |
| Fri, 25 Nov 2005 18:58:36 +0100 | wenzelm | fix_tac: proper treatment of major premises in goal; | changeset | files |