| 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 |
| Wed, 27 Jan 2010 14:03:08 +0100 | haftmann | merged | changeset | files |
| Wed, 27 Jan 2010 14:02:53 +0100 | haftmann | a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML | changeset | files |
| Wed, 27 Jan 2010 14:02:53 +0100 | haftmann | lemma Image_closed_trancl | changeset | files |
| Wed, 27 Jan 2010 14:02:52 +0100 | haftmann | corrected type of typecopy constructor | changeset | files |