[isabelle] Automaton example



I started to study the representation of input/output automata in Isabelle.
I opened the example Cockpit.thy in the directory HOLCF/IOA/Modelcheck and I
started the analysis. Isabelle loads MuIOAOracle but when reach the keyword
"automaton" it stops with the error message:

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

Why?
I read the article about IOA but I didn't understand where is the problem.
Can anyone help me?

Thanks
Gabriele




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