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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
