[isabelle-dev] Declaration depending on user proofs

[Alexander Krauss]

> 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 ...

Your mileage may vary, depending on the PG version used. For me it lead 
to very frequent synchronization losses, so I quickly gave up...

Alex