*To*: Marco Maggesi <maggesi at math.unifi.it>*Subject*: Re: [isabelle] datetypes in Isabelle/ZF*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 8 Oct 2008 10:29:46 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <0FE00F8C-4568-40BF-B236-6EE46555C096@math.unifi.it>*References*: <0FE00F8C-4568-40BF-B236-6EE46555C096@math.unifi.it>

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

**References**:**[isabelle] datetypes in Isabelle/ZF***From:*Marco Maggesi

- Previous by Date: [isabelle] New AFP entry: Arrow's Impossibility Theorem
- Next by Date: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Previous by Thread: [isabelle] datetypes in Isabelle/ZF
- Next by Thread: [isabelle] Nominal logic in Isabelle 2005 / Re: Incompatibilities between releases
- Cl-isabelle-users October 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list