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



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

Cheers
Lars




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