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

[Florian Haftmann]

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

The import could be changed e.g. to Groups_List.

Desirable would also be to split the theory into Factorial and Binomial,
to raise awareness of existing combinatorial material in HOL.

As an aside, maybe someone is eager to take the comment

> (*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)

seriously.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170425/f5363029/attachment.sig>