Wed, 27 Feb 2008 14:39:48 +0100 | chaieb | Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy | changeset | files |
Tue, 26 Feb 2008 20:38:18 +0100 | haftmann | other UNIV lemmas | changeset | files |
Tue, 26 Feb 2008 20:38:17 +0100 | haftmann | some more primrec | changeset | files |
Tue, 26 Feb 2008 20:38:16 +0100 | haftmann | class itself works around a problem with class interpretation in class finite | changeset | files |
Tue, 26 Feb 2008 20:38:15 +0100 | haftmann | moved some set lemmas from Set.thy here | changeset | files |
Tue, 26 Feb 2008 20:38:14 +0100 | haftmann | tuned heading | changeset | files |
Tue, 26 Feb 2008 20:38:13 +0100 | haftmann | char and nibble are finite | changeset | files |