[isabelle] arities syntax in Isar-style theory files




The reference manual gives the following example

arities
  foo :: ({logic}) logic
  foo :: ({}) term

(which is syntactically accepted in an old-style theory though
it produces an error)

But in an Isar-style theory it is rejected with the following
message

*** Outer syntax error (line 33 of "/home/users/jeremy/isabelle/cat/kozen.thy"): sort expected, *** but command "{" (line 33 of "/home/users/jeremy/isabelle/cat/kozen.thy") was found

The Isar ref manual documentation leaves me confused.

Does anyone know what is the Isar equivalent for the example above?

Jeremy






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