# HG changeset patch
# User wenzelm
# Date 969042840 -7200
# Node ID fe6ffa46266fbd3d9037080b773945ce5689b4c5
# Parent  566c6b90637089ed8cac4ee68b9470985b0ef1a2
someI2_ex;

diff -r 566c6b906370 -r fe6ffa46266f doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Sep 15 20:22:36 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Sep 15 20:34:00 2000 +0200
@@ -142,11 +142,11 @@
 apply(intro strip);
 apply(induct_tac i);
  apply(simp);
- apply(fast intro:someI2EX);
+ apply(fast intro:someI2_ex);
 apply(simp);
-apply(rule someI2EX);
+apply(rule someI2_ex);
  apply(blast);
-apply(rule someI2EX);
+apply(rule someI2_ex);
  apply(blast);
 by(blast);
 
@@ -162,11 +162,11 @@
 apply(intro strip);
 apply(induct_tac i);
  apply(simp);
- apply(fast intro:someI2EX);
+ apply(fast intro:someI2_ex);
 apply(simp);
-apply(rule someI2EX);
+apply(rule someI2_ex);
  apply(blast);
-apply(rule someI2EX);
+apply(rule someI2_ex);
  apply(blast);
 by(blast);