>> 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.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
