| Mon, 08 Feb 2010 14:12:50 +0100 | haftmann | avoid upto in generated code (is infix operator in library.ML) | changeset | files |
| Mon, 08 Feb 2010 15:25:00 +0100 | haftmann | separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4 | changeset | files |
| Mon, 08 Feb 2010 14:08:32 +0100 | haftmann | merged | changeset | files |
| Mon, 08 Feb 2010 14:06:58 +0100 | haftmann | more precise proofs | changeset | files |
| Mon, 08 Feb 2010 14:06:54 +0100 | haftmann | moved auxiliary lemmas to more appropriate places | changeset | files |
| Mon, 08 Feb 2010 14:06:51 +0100 | haftmann | separate library theory for type classes combining lattices with various algebraic structures; more simp rules | changeset | files |
| Mon, 08 Feb 2010 14:06:48 +0100 | haftmann | dropped instantiations for combined lattices | changeset | files |
| Mon, 08 Feb 2010 14:06:46 +0100 | haftmann | added lemmas involving Min, Max, uminus | changeset | files |