[isabelle] Modelcheck example



I proved to use the examples about the integration between Isabelle and
Mucke.
I have installed Isabelle 2005 and Mucke 0.4.4.

Isabelle analyse theory MuckeExample1 (in HOL/Modelcheck) but when it
reaches lemma "reach_ex1" and in particular the application of the second
tactic it stops with the follow error:
*** exception THM raised: instantiate: type conflict
***   ?a::bool × bool × bool => bool :: bool × bool × bool => bool
***   ?a1::?'a :: ?'a
*** At command "apply".

While when it reaches the second lemma "reach_ex" it stops with the error:
*** Inner lexical error at: "INIT == % x . ¬ fst (x::bool × bool × bool) AND
¬ fst (snd x) AND ¬ snd (snd x)"
*** The error(s) above occurred for "INIT == % x . ¬ fst (x::bool × bool ×
bool) AND ¬ fst (snd x) AND ¬ snd (snd x)"
*** At command "by".

Can anyone help me?
Thanks in advance for the collaboration.

Gabriele




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