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