[isabelle] Argument types problem



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

inductive_set
  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.




--gh



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