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

[Lawrence Paulson]

This makes perfect sense to me.

I suggest moving at least the definition of Fpow into Main (it’s small, and fundamental) while creating a new Library entry for my own new material.

Larry

> On 23 Jan 2019, at 12:48, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote:
> 
> 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
>