Re: [isabelle] Subset Types



Ashley,

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.

cheers
peter

-- 
http://peteg.org/






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