Sun, 31 Jan 2010 14:51:30 +0100 | haftmann | more correspondence lemmas between related operations; tuned some proofs | changeset | files |
Thu, 28 Jan 2010 11:48:49 +0100 | haftmann | new theory Algebras.thy for generic algebraic structures | changeset | files |
Thu, 28 Jan 2010 11:48:43 +0100 | haftmann | dropped mk_left_commute; use interpretation of locale abel_semigroup instead | changeset | files |