Re: [isabelle] datetypes in Isabelle/ZF



It would appear that this documentation requires updating. Meanwhile, you'll find the correct version of this example in the file src/ZF/ Induct/Term.thy.

Larry Paulson


On 7 Oct 2008, at 16:22, Marco Maggesi wrote:

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.