[isabelle] Argument types problem

Dear fellows,
I am about to definie an inductive set to compute the ste of reachable
states as following:

  Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set" where
     init: "s ∈ Init ==> s ∈ (Reachable Ts Init)"
     | nextStep : "==> [| s ∈ (Reachable Ts Init); (mk_trans s a t) ∈
(trans_of Ts) |] ==> t ∈ (Reachable Ts Init)"

But it was not accepted and I got the following error message:
Argument types ('action, 'state) ts, 'state set of Reachable do not agree
with types of declared parameters

Any helps how to sort out this error please.


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