[isabelle-dev] Additional type variable(s) in specification

Lawrence Paulson lp15 at cam.ac.uk
Thu Dec 2 16:09:46 CET 2010

I agree!

On 2 Dec 2010, at 14:44, Brian Huffman wrote:

> Besides these two very specific cases, I think it would be best to
> reject definitions with extra type variables on the right-hand side.

More information about the isabelle-dev mailing list