[isabelle] Error in automaton example
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
*** (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
Similar errors occur with other examples and with a my theory.
Can anyone help me?
Thanks in advance for the help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and