Re: [isabelle] Automaton example
On Thu, 31 Aug 2006, Gabriele Pozzani wrote:
> *** Outer syntax error: command expected,
> *** but identifier "automaton" was found
> I read the article about IOA but I didn't understand where is the problem.
You need to use the proper logic image, i.e. IOA (which is derived from
HOLCF). You can produce it like this:
Isabelle2005/build -m IOA HOLCF
Then run Isabelle with -l IOA option, or select the image manually from
the ProofGeneral menu.
This archive was generated by a fusion of
Pipermail (Mailman edition) and