Re: [isabelle] type_synonym

Am 12/08/2012 22:03, schrieb Makarius:
> On Sat, 11 Aug 2012, Tobias Nipkow wrote:
>> surely one could also wrap that code up into a top level command?
> I would rather make it a variant of the existing 'typ' command like this:
>   typ T  -- "as before"
>   typ T :: S  -- "with sort check"

Great minds think alike ;-)
I hadn't suggested it myself because I thought you might object that this gives
the impression that "T :: S" is legal syntax for types in general.
But I am all for it!


> I'll study the situation of the sources soon ...
>     Makarius

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