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.


Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to