--- a/doc-src/TutorialI/CTL/CTL.thy Fri Sep 15 19:34:28 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Fri Sep 15 19:59:05 2000 +0200
@@ -142,11 +142,11 @@
apply(intro strip);
apply(induct_tac i);
apply(simp);
- apply(fast intro:selectI2EX);
+ apply(fast intro:someI2EX);
apply(simp);
-apply(rule selectI2EX);
+apply(rule someI2EX);
apply(blast);
-apply(rule selectI2EX);
+apply(rule someI2EX);
apply(blast);
by(blast);
@@ -162,11 +162,11 @@
apply(intro strip);
apply(induct_tac i);
apply(simp);
- apply(fast intro:selectI2EX);
+ apply(fast intro:someI2EX);
apply(simp);
-apply(rule selectI2EX);
+apply(rule someI2EX);
apply(blast);
-apply(rule selectI2EX);
+apply(rule someI2EX);
apply(blast);
by(blast);