Re: [isabelle] Error in automaton example
On Mon, 11 Sep 2006, Gabriele Pozzani wrote:
> 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 cannot reproduce this problem. It works for me as follows:
* Start Isabelle2005 with the IOA image
* Issue the following ML code from src/HOLCF/IOA/Modelcheck/ROOT.ML:
with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle";
* Visit src/HOLCF/IOA/Modelcheck/Cockpit.thy and assert the whole
This archive was generated by a fusion of
Pipermail (Mailman edition) and