[isabelle] ax_specification parse error



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






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