--- a/doc-src/TutorialI/Inductive/Star.thy Tue Apr 17 16:54:38 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy Tue Apr 17 19:28:04 2001 +0200
@@ -91,7 +91,7 @@
txt{*\noindent
This is not an obscure trick but a generally applicable heuristic:
\begin{quote}\em
-Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
+When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
pull all other premises containing any of the $x@i$ into the conclusion
using $\longrightarrow$.
\end{quote}