Re: [isabelle] Cardinality for infinite sets

Hi Diego,

Please see

and, for a more complete set of results,

These are all documented in the ITP 2014 paper

Let me know should you have any problems using these.



From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Diego Marmsoler <diego.marmsoler at>
Sent: 21 March 2018 18:19:24
To: isabelle-users at
Subject: [isabelle] Cardinality for infinite sets

Dear Isabelle experts,

while playing around with "card" from theory Finite_Set, i recognized that it returns 0 for infinite sets.
Now i was wondering whether someone knows about a similar construct which, for this case, returns infinity from the extended natural numbers.

Many thanks in advance!

Best regards,


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