doc-src/TutorialI/CTL/CTL.thy

 apply(rule_tac x = "path s P" in exI);
 apply(simp);
 apply(intro strip);
 apply(induct_tac i);
  apply(simp);
- apply(fast intro:selectI2EX);
-apply(simp);
-apply(rule selectI2EX);
- apply(blast);
-apply(rule selectI2EX);
+ apply(fast intro:someI2EX);
+apply(simp);
+apply(rule someI2EX);
+ apply(blast);
+apply(rule someI2EX);
  apply(blast);
 by(blast);
 
 lemma seq_lemma:
 "\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow>

 apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)" in exI);
 apply(simp);
 apply(intro strip);
 apply(induct_tac i);
  apply(simp);
- apply(fast intro:selectI2EX);
-apply(simp);
-apply(rule selectI2EX);
- apply(blast);
-apply(rule selectI2EX);
+ apply(fast intro:someI2EX);
+apply(simp);
+apply(rule someI2EX);
+ apply(blast);
+apply(rule someI2EX);
  apply(blast);
 by(blast);
 
 theorem AF_subset_lfp:
 "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";