diff -r 32d76edc5e5c -r ca73e86c22bb doc-src/TutorialI/Inductive/document/Star.tex
--- a/doc-src/TutorialI/Inductive/document/Star.tex	Thu Jul 19 15:35:00 2007 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Thu Jul 19 15:35:36 2007 +0200
@@ -91,7 +91,8 @@
 \isaindent{\ \ \ \ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline
 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}%
 \end{isabelle}
-It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition,
+It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}}
+if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition,
 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the
 premises. In general, rule induction for an $n$-ary inductive relation $R$
 expects a premise of the form $(x@1,\dots,x@n) \in R$.