[isabelle-dev] NEWS: GCD and Binomial in Main
makarius at sketis.net
Sun May 14 12:45:24 CEST 2017
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev