[isabelle-dev] Declaration depending on user proofs

Makarius makarius at sketis.net
Wed Nov 3 11:20:20 CET 2010


On Wed, 3 Nov 2010, Florian Haftmann wrote:

> Of course the Ā»globalĀ« nature of keywords makes it difficult to do 
> ad-hoc experimentation with new keywords, one generic slot would 
> simplify this.  Again, this is no pressing issue.

I would say it is virtually impossible to experiment with new commands in 
Proof General.  One needs to produce isabelle-keywords.el in batch mode 
first, and then continue interactively. The situation will become much 
better in the new document model, but the restriction of theory boundaries 
is most likely here to stay.


 	Makarius


More information about the isabelle-dev mailing list