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.


> On 23 Jan 2019, at 12:48, Blanchette, J.C. <> 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

isabelle-dev mailing list

Reply via email to