[isabelle] Error in automaton example



Dear all,
I have opened and analyzed the Cockpit example about IOA but when Isabelle
reaches automaton Al_before_Ack it stops with the follow error

*** Type unification failed
*** Type error in application: Incompatible operand type
***
*** Operator:
***   (action_case
***     (l(a::event).
***         (True OR
***          ((APonR_incl'::bool) =
***           (if (a = PonR) then True else (APonR_incl::bool)))))) ::
***   (event => bool) => (event => bool) => event action => bool
*** Operand:   (l(a::?'a). False) :: ?'a => bool
***
*** The error(s) above occurred in axiom "Al_before_Ack_trans_def"
*** At command "automaton".

I don't understand where is the problem.
The type unification is internal to this automaton or with the previous
automata?

Similar errors occur with other examples and with a my theory.

Can anyone help me?

Thanks in advance for the help.

Gabriele




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