src/HOL/Finite_Set.thy
changeset 22473 753123c89d72
parent 22451 989182f660e0
child 22616 4747e87ac5c4
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -2533,7 +2533,7 @@
     1.4  
     1.5  subsection {* Class @{text finite} *}
     1.6  
     1.7 -class finite (attach UNIV) =
     1.8 +class finite (attach UNIV) = type +
     1.9    assumes finite: "finite UNIV"
    1.10  
    1.11  lemma finite_set: "finite (A::'a::finite set)"