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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and