Re: [isabelle] Showing that type 'int' is infinite
this is theorem nat_infinite (or nat_not_finite) from theory Infinite_Set.
All the best,
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?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and