[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.