[isabelle] ax_specification parse error
I am trying to use the ax_specification form in Isabelle, because I
might use theory interpretations down the road, and so I don't want
the constant to be defined in terms of the Hilbert choice operator.
However, when I try to use ax_specification, e.g.
consts foo :: "int => bool"
foo_def: "EX x. foo x"
I get the following Isabelle parse error:
*** Outer syntax error: name declaration expected,
*** but keyword "(" was found
On the other hand, Isabelle accepts the declaration if I change
"ax_specification" to "specification".
This archive was generated by a fusion of
Pipermail (Mailman edition) and