[isabelle-dev] Declaration depending on user proofs

[Brian Huffman]

On Wed, Nov 3, 2010 at 3:32 AM, Alexander Krauss <krauss at in.tum.de> wrote:
> 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 accident.

I have done plenty of experiments with new commands in Proof General,
without ever modifying the keywords file. All you need to do is use a
command that ends with a semicolon immediately before each new
command, like this:

text "";
new_experimental_command ...

- Brian