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.


isabelle-dev mailing list

Reply via email to