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. 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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
