Re: [isabelle] Automaton example



Hi Gabriele,

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

You are using the wrong keyword file for ProofGeneral. In order to know what are keywords, ProofGeneral uses a keyword file which is generated by Isabelle and is located in "$ISABELLE_HOME/etc/isar-keywords.el". In fact, the standard keyword file should already know about IOA...

What version are you using?

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.

Hope that helps,
Alex





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