# Re: [isabelle] Showing that type 'int' is infinite

John,
this is theorem nat_infinite (or nat_not_finite) from theory Infinite_Set.
All the best,
Stephan
John Matthews wrote:

I have a subgoal of the form
1. "~ (finite (UNIV :: int set))"

`However, I can't find a corresponding theorem using find_theorems in
``Isabelle/HOL. Nor was find_theorems produce successful on the terms
``"card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".
`
What is the best way to prove this subgoal?
Thanks,
-john

begin:vcard
fn:Stephan Merz
n:Merz;Stephan
org:INRIA Lorraine & LORIA
adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France
email;internet:Stephan.Merz at loria.fr
tel;work:(+33) 354 95 84 78
tel;fax:(+33) 383 41 30 79
x-mozilla-html:FALSE
url:http://www.loria.fr/~merz/
version:2.1
end:vcard

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*