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.


	Makarius





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