| 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 |
| Sun, 10 Jan 2010 18:06:30 +0100 | berghofe | Tuned some proofs; nicer case names for some of the induction / cases rules. | changeset | files |
| Sun, 10 Jan 2010 18:03:20 +0100 | berghofe | Added setup for simplification of equality constraints in induction rules. | changeset | files |
| Sun, 10 Jan 2010 18:01:04 +0100 | berghofe | Added infrastructure for simplifying equality constraints. | changeset | files |