doc-src/TutorialI/Inductive/Star.thy

--- a/doc-src/TutorialI/Inductive/Star.thy	Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy	Fri May 18 16:45:55 2001 +0200
@@ -36,7 +36,7 @@
 the standard definition. We start with a simple lemma:
 *}
 
-lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
+lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
 by(blast intro: rtc_step);
 
 text{*\noindent