[isabelle] Problems with datatype definition
the following datatype definition is not accepted in Isabelle/HOL,
presumably since the parameter of foo has been changed to "'a option".
datatype 'a foo = Bar 'a | Com "'a option foo"
Is there some known workaround for this problem?
Thanks in advance,
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
This archive was generated by a fusion of
Pipermail (Mailman edition) and