Email Gateway (Aug 18 2022 at 12:29): Email Gateway (Aug 18 2022 at 12:29):From: Marco Maggesi <maggesi@math.unifi.it>
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
Email Gateway (Aug 18 2022 at 12:29):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: May 03 2024 at 04:19 UTC