src/HOL/Finite.thy

--- a/src/HOL/Finite.thy	Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Finite.thy	Wed Oct 27 19:32:19 1999 +0200
@@ -18,6 +18,9 @@
 syntax finite :: 'a set => bool
 translations  "finite A"  ==  "A : Finites"
 
+axclass	finite<term
+  finite "finite UNIV"
+
 (* This definition, although traditional, is ugly to work with
 constdefs
   card :: 'a set => nat