[isabelle-dev] NEWS: GCD and Binomial in Main

[Makarius]

*** 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