diff -r 891fbd3f4881 -r b28bbb153603 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 \ (x,y) \ r*" +lemma [intro]: "(x,y) \ r \ (x,y) \ r*" by(blast intro: rtc_step); text{*\noindent