[isabelle-dev] A possible bug with Isabelle 2013
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
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