[isabelle] Defining Union Types

Dear Isabelle Users,

Do we have in Isabelle something like a union (sum) type constructor with
the corresponding injections?
I went through the tutorial and did not  find use or reference to it. If
there is, can anyone point to an application
or a written example of  this?

I assume there must be a simple way to do it.

Many thanks!

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil

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