[isabelle-dev] NEWS

Makarius makarius at sketis.net
Sat Mar 13 21:19:16 CET 2010

* Pure: local theory specifications may depend on extra type variables 
that are not present in the result type -- arguments TYPE('a) :: 'a itself 
are added internally.  For example:

   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"

More information about the isabelle-dev mailing list