> * Theories "GCD" and "Binomial" are already included in "Main" (instead > of "Complex_Main"). > > > This refers to Isabelle/f533820e7248: the change came up while exploring > theory imports systematically. Normally, only "Main" or "Complex_Main" > should be imported from the HOL session, not anything in between. (This > is a concession to the complex bootstrap process of HOL.) > > In Isabelle/85ed070017b7 Florian has already improved the imports of GCD > further. > > 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.
As an aside, maybe someone is eager to take the comment
> (*TODO: This code equation breaks Scala code generation in
> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
seriously.
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
