[isabelle-dev] Declaration depending on user proofs

[Makarius]

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