[isabelle] datetypes in Isabelle/ZF



Hi,

I new to Isabelle and especially to Isabelle/ZF (I have some limited
experience with Isabelle/HOL though).

The following definition (taken from the logics-ZF.pdf page 54)
fails on my system (Isabelle/ZF 2008):

----------------------------------------------------------------------
theory DT imports Main_ZF begin

consts "term" :: "i => i"
datatype "term(A)" = Apply ("a:A","l:list(term(A))")
  monos list_mono
----------------------------------------------------------------------

with the following error message:

*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** [| a : A; l : list(term(A)) |] ==> Apply(a, l) : term(A)
*** At command "datatype".

How can I fix this?

Thanks in advance,
Marco






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