[isabelle-dev] [Spam] cardinality primitives in Isabelle/HOL?

[Blanchette, J.C.]

Hi Larry,

You wrote:

> The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so clearly a lot of facts about cardinals are available already in Main.

FYI: As you might already know or deduced from the name convention, the (co)datatype (a.k.a. "BNF") package is based on some cardinality material. When we moved the BNF package into Main, I surgically split the HOL-Cardinals theories into two, moving the exact dependencies into Main and leaving the rest outside. As a result, it's pretty random what's in Main and what's outside. The alternative -- moving all of HOL-Cardinals into Main -- seemed undesirable because it would slow down building Main quite a bit.

Jasmin