Tue, 05 Oct 2010 11:45:16 +0200 | haftmann | merged | changeset | files |
Tue, 05 Oct 2010 11:37:42 +0200 | haftmann | lemmas fold_commute and fold_commute_apply | changeset | files |
Fri, 07 May 2010 15:36:03 +0200 | krauss | spelling | changeset | files |
Mon, 04 Oct 2010 14:46:49 +0200 | haftmann | adjusted to inductive characterization of sorted | changeset | files |
Mon, 04 Oct 2010 14:46:49 +0200 | haftmann | tuned whitespace | changeset | files |
Mon, 04 Oct 2010 14:46:48 +0200 | haftmann | turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs | changeset | files |