Re: [isabelle] Subset Types


On 11/11/2011, at 10:39 AM, Ashley Yakeley wrote:

> Is it possible to create types that are subsets of an existing type?

This is precisely what typedef does.

See Section 8.5 in the Isabelle tutorial (accompanying the distribution).

There are also lots of examples in the HOL source itself.



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