| Fri, 15 Jan 2010 13:37:41 +0100 | berghofe | Eliminated is_open option of Rule_Cases.make_nested/make_common; | changeset | files |
| Sun, 10 Jan 2010 18:43:45 +0100 | berghofe | Adapted to changes in induct method. | changeset | files |
| Sun, 10 Jan 2010 18:41:07 +0100 | berghofe | Adapted to changes in setup of induct method. | changeset | files |
| Sun, 10 Jan 2010 18:39:50 +0100 | berghofe | Expand proofs of induct_atomize'/rulify'. | changeset | files |
| Sun, 10 Jan 2010 18:37:37 +0100 | berghofe | Changed case names of converse_rtranclp_induct. | changeset | files |
| Sun, 10 Jan 2010 18:11:00 +0100 | berghofe | Injectivity / distinctness theorems are now used to simplify induction rules. | changeset | files |
| Sun, 10 Jan 2010 18:09:11 +0100 | berghofe | same_append_eq / append_same_eq are now used for simplifying induction rules. | changeset | files |