[isabelle-dev] NEWS: GCD and Binomial in Main
makarius at sketis.net
Mon Apr 24 15:55:23 CEST 2017
*** HOL ***
* Theories "GCD" and "Binomial" are already included in "Main" (instead
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
Are there good ideas how to do it with Binomial? Thus we could get rid
of the Pre_Main theory from f533820e7248.
More information about the isabelle-dev