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

[Makarius]

On Thu, 2 Dec 2010, Tobias Nipkow wrote:

> The interface is a red herring. The discussion is on the concept at the 
> user level.

Here is again a current snapshot with everything built and bundled 
http://www.lri.fr/~wenzel/Isar2010-Orsay/download.html

The new interaction model seriously changes the rules of the game.  In the 
past few month I've had many surprises how the system outputs information 
to the user, which turned out as historical artifacts due to the 
accidental Proof General message model.


Since the current issue is about user confusion, the user interface model 
needs to be taken into account.

When the Prover IDE is starting to replace Proof General more seriously, 
many messages, warnings, errors will have to be revised.  I have already 
started to think about the problem of implicit introduction of 
polymorphism into the context in its many guises.  Of course, I am 
interested in good ideas from the standpoint of the new technology, i.e. 
from anybody who has seriously tried Isabelle/jEdit already.


 	Makarius