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

[Makarius]

On 13/05/17 08:16, Florian Haftmann wrote:
>>> 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.
> 
> See now bdd17b18e103.
> 
> Theory Pre_Main is still present, but now trivial to get rid of.

Great. I've done that now in 3039d4aa7143.


	Makarius



-------------- 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/20170514/7f1ba37e/attachment.sig>