[isabelle] Datatype Morphisms in Isabelle

Dear Isabelle Users,

This is a very simple question:

Assume a language L specifiied by a datatype D, where L = Lang(D). If L is
a subset of L', how
can I write in Isabelle a datatype D', that extends D  such that Lang(D')=

More generally, how can I model datatype morphisms in Isabelle, so that the
case above
is just a simple inclusion arrow.

Many thanks!
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

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