[isabelle-dev] Declaration depending on user proofs
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.
More information about the isabelle-dev