[isabelle] Showing that type 'int' is infinite



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






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