[isabelle] Modelcheck example
I proved to use the examples about the integration between Isabelle and
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and