[isabelle-dev] NEWS: GCD and Binomial in Main

Manuel Eberl eberlm at in.tum.de
Tue Apr 25 11:06:33 CEST 2017

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. *)


More information about the isabelle-dev mailing list