[isabelle-dev] A possible bug with Isabelle 2013

Makarius makarius at sketis.net
Fri Mar 1 13:45:00 CET 2013

On Fri, 1 Mar 2013, Lawrence Paulson wrote:

> In Edinburgh LCF, term quotations containing anonymous type variables 
> were simply rejected. Perhaps that would still be the best approach now. 
> I'm not convinced that it would lead to more errors than the 'a itself 
> approach.

I know, you've explained that to me many years ago.

For us now, it means to mark-up these critical spots where polymoprhism 
emerges.  The information can then be somehow visualized for the user. 
It is also possible to get a systematic overview over all reachable 
Isabelle applications (including AFP) how things actually happens in the 

The latter is not just for empirical exploration of sources.  With formal 
markup of certain kind over the text, that can be "refactored" 
systematically.  I am here not so much thinking of eliminating legitimate 
uses of polymorphism, but things like cleaning up notation to avoid the 
mix of --> and ⟶ symbols.


More information about the isabelle-dev mailing list