--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Jun 12 14:20:25 2008 +0200
@@ -346,8 +346,8 @@
\isatagproof
%
\begin{isamarkuptxt}%
-The proof script is identical, but the subgoal after applying induction may
-be surprising:
+The proof script is virtually identical,
+but the subgoal after applying induction may be surprising:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline