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

Blanchette, J.C. j.c.blanchette at vu.nl
Wed Jan 23 13:48:30 CET 2019

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.


More information about the isabelle-dev mailing list