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

Makarius makarius at sketis.net
Mon Apr 24 15:55:23 CEST 2017

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

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 mailing list