Re: [isabelle] Defining Union Types

It is written "+" and defined in theory Sum_Type, which is part of Main.
It is hardly advertised because in most cases it is nicer to define your
own special datatype.


Am 26/07/2011 03:57, schrieb Alfio Martini:
> 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!

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