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

[Makarius]

On Thu, 2 Dec 2010, Brian Huffman wrote:

> If the default behavior of the "typedef" command was to work like 
> "typedef (open)" (and I think it ought to be), then there would have 
> been no problem

There would have been no problem in this example, but the problem still 
exists in general, and had been known to me for many years already.  The 
pitfalls of hidden polymorphism date even back to very early versions of 
Gordon HOL -- initially they made use of it in an unsound way.

If or not typedef should define a the set is a completely different 
question.  It does so, because Larry introduced the scheme like that many 
many years ago, and the normal way is not to change things at will, unless 
there are reasons for it.  Over time a certain (initially arbitrary) 
decision tends to become harder to reform, but this is also done if the 
reasons are strong enough.


 	Makarius