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