| 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 |