[isabelle-dev] Declaration depending on user proofs

Alexander Krauss krauss at in.tum.de
Wed Nov 3 14:13:36 CET 2010


> 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



More information about the isabelle-dev mailing list