the code for bar does not compile, since parenthesis are missing
around its argument do-block.
thanks for reporting this. Until this is resolved, you may want help
yourself dropping the »code_monad« declaration in the Imperative_HOL
sources.
See now 271829a473ed.
Florian
--
On 25.09.2014 18:32, Tobias Nipkow wrote:
Florian: But you agree that it should be uniformaly Sum or sum for all
summation operators? Johannes already remarked on the discrepancy in your
proposal.
That would be »Sum_list« and »Prod_list«.
The idea of having »sum« and »prod« was inspired by
