Hi Fréderic,
see now
http://isabelle.in.tum.de/repos/isabelle/rev/774752af4a1f
http://isabelle.in.tum.de/repos/isabelle/rev/8e736ce4c6f4
>> By comparing the generating code for SML and OCaml in
>> src/Tools/Code/code_ml.ML, I would be tempted to replace
>> "brackify_block" by "brackets"
Hi Frédéric,
thanks for going into this so thoroughly.
I will look after these errors as soon possible.
In ancient days, there was a dedicated theory which contained such
»challenges« for the code generator, but with more and more theories
with code generation this had been given up; maybe
