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