*** HOL ***
* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").
This refers to Isabelle/f533820e7248: the change came up while exploring
theory imports systematically. Normally, only "Main" or "Complex_Main"
should be imported from the HOL session, not anything in between. (This
is a concession to the complex bootstrap process of HOL.)
In Isabelle/85ed070017b7 Florian has already improved the imports of GCD
further.
Are there good ideas how to do it with Binomial? Thus we could get rid
of the Pre_Main theory from f533820e7248.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
