[isabelle-dev] Declaration depending on user proofs

Alexander Krauss krauss at in.tum.de
Wed Nov 3 11:32:38 CET 2010

Makarius wrote:
> 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.

My standard workaround is to edit isar-keywords.el manually, ignoring 
the WARNING IN CAPITAL LETTERS. This is OK for local experiments. I 
typically first copy the file to my .isabelle, so I cannot commit it by 


More information about the isabelle-dev mailing list