Re: [isabelle] type_synonym

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"

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


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