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