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
