Re: [isabelle] value (code) doesn't complain when no code equations exist



2015-06-03 11:53 GMT+02:00 Lars Hupel <hupel at in.tum.de>:
>> value [code] "expression"
>
> Thanks, that was the missing bit: I was using wrong syntax! I thought
> that 'value (code)' was the way to select the evaluation strategy, but
> in fact, I can write anything there ... 'value (foobar)' gets happily
> accepted :-)

Why did I also use value(code) all the time? Was this in some release candidate?

find ./ -name '*.thy' | xargs grep 'value(code)' | wc -l
25

This explains a lot! Thanks!

  Cornelius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.