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_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
