changeset 12338 | de0f4a63baa5 |
parent 12114 | a8e860c86252 |
--- a/src/HOL/Finite.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/Finite.thy Sat Dec 01 18:52:32 2001 +0100 @@ -18,7 +18,7 @@ syntax finite :: 'a set => bool translations "finite A" == "A : Finites" -axclass finite<term +axclass finite < type finite "finite UNIV" (* This definition, although traditional, is ugly to work with