Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: John Matthews <matthews@galois.com>
Hi,
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"
ax_specification (foo)
foo_def: "EX x. foo x"
by auto
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".
Thanks,
-john
Last updated: May 03 2024 at 08:18 UTC