Re: [isabelle-dev] NEWS: GCD and Binomial in Main
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
Re: [isabelle-dev] NEWS: GCD and Binomial in Main
>> 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
Re: [isabelle-dev] NEWS: GCD and Binomial in Main
Before I forget: I did that and it is as expected; everything still works. Manuel On 2017-04-25 11:12, Florian Haftmann wrote: Am 25.04.2017 um 11:06 schrieb Manuel Eberl: I think you actually solved that problem by now. If I recall correctly, it was one of the two dictionary-related problems I told you about a year ago or so, and then Lars and you solved that problem somehow. I can try putting in that code equation again and seeing what happens. Excellent, thanks. Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: GCD and Binomial in Main
Am 25.04.2017 um 11:06 schrieb Manuel Eberl: > I think you actually solved that problem by now. If I recall correctly, > it was one of the two dictionary-related problems I told you about a > year ago or so, and then Lars and you solved that problem somehow. > > I can try putting in that code equation again and seeing what happens. Excellent, thanks. Florian > > >>> (*TODO: This code equation breaks Scala code generation in >>> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. >>> *) > > Manuel > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- 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
Re: [isabelle-dev] NEWS: GCD and Binomial in Main
I think you actually solved that problem by now. If I recall correctly, it was one of the two dictionary-related problems I told you about a year ago or so, and then Lars and you solved that problem somehow. I can try putting in that code equation again and seeing what happens. >> (*TODO: This code equation breaks Scala code generation in >> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *) Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: GCD and Binomial in Main
> * 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
[isabelle-dev] NEWS: GCD and Binomial in Main
*** HOL *** * 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
