[isabelle] Error in simproc



Dear All,

I keep getting errors resembling the following when trying to invoke simp.

*** Error in simproc "let_simp":
*** Error in simproc "split_beta":
*** Proof failed.
*** (l(turn', trys').
***     let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts, Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
***         ((turn', trys'), bool_case :084 pc'))
***  (Rsharedf (:081, :082)) =
*** (let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts, Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
***      (Rsharedf (:081, :082), bool_case :084 pc'))
***  1. (l(turn', trys').
***         let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts, Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
***             ((turn', trys'), bool_case :084 pc'))
***      (Rsharedf (:081, :082)) =
***     (let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts, Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
***          (Rsharedf (:081, :082), bool_case :084 pc'))
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** (l(turn', trys').
***     let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts, Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
***         ((turn', trys'), bool_case :084 pc'))
***  (Rsharedf (:081, :082)) =
*** (let pc' = Rexpf :083
*** in Abstraction.trans (Peterson2.peterson_starts, Peterson2.peterson_trans False) ((:089, :090), bool_case :084 :091)
***      (Rsharedf (:081, :082), bool_case :084 pc'))
*** At command "apply".

Does anyone know what is going on?

Thanks

Tom





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