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
>> 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
