doc-src/TutorialI/CTL/CTLind.thy

 A}-avoiding path:
 % Second proof of opposite direction, directly by well-founded induction
 % on the initial segment of M that avoids A.
 *}
 
-consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
-inductive "Avoid s A"
-intros "s \<in> Avoid s A"
-       "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
+inductive_set
+  Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set"
+  for s :: state and A :: "state set"
+where
+    "s \<in> Avoid s A"
+  | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
 
 text{*
 It is easy to see that for any infinite @{term A}-avoiding path @{term f}
 with @{prop"f(0::nat) \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
 starting with @{term s} because (by definition of @{const Avoid}) there is a