[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
I read the article about IOA but I didn't understand where is the problem.
Can anyone help me?
This archive was generated by a fusion of
Pipermail (Mailman edition) and