[isabelle] Fwd: problem with inductive definition



Dear fellows
I am new to Isabelle/HOL and I was trying to define something in an
inductive way as follows:

inductive
  Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set" where
  here: "s ∈ I ==> s ∈ Reachable S I"
 | onemore : "[| s ∈ (Reachable S I); mk_trans s a t ∈ trans_of S |] ==> t
∈ (Reachable S I)"


But I got an error message:
ill-formed introduction rule "here"
s ∈ I ==> s ∈ Reachable S I
Conclusion of introduction must be an inductive predicate

Any helps will be very appreciated



Regards
--gh



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