Re: [isabelle] Automaton example

On 9/1/06, Alexander Krauss <krauss at> wrote:

Hi Gabriele,

> *** Outer syntax error: command expected,
> *** but identifier "automaton" was found

You can re-generate the keyword file by issuing the command

ML {* ProofGeneral.write_keywords "" *}

after you have loaded all the theories you are using.
Then copy the created file "isar-keywords.el" to the above location.

I proved to re-generate the keyword file but nothing change. I opened
isar-keywords.el in a text-editor and the keyword automaton is present.

I re-built the logic image as suggested by Makarius but, again, nothing

Do you have other ideas?

Thanks for the collaboration.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.