Re: [isabelle] Extra type variables in constdef



On Fri, 21 Sep 2007, Florian Haftmann wrote:

> constsdefs
>   c :: "'a itself => int => bool"
>   "c (T::'a itself) x == b (a x :: 'a)"

Just note that there is no need to invent a dummy argument T here, because 
the canonical term TYPE('a) of type 'a itself will do the trick.


	Makarius





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