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
This explains a lot! Thanks!
This archive was generated by a fusion of
Pipermail (Mailman edition) and