diff -r b87b41ade3b2 -r deae80045527 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Jan 10 01:13:41 2002 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Jan 10 11:22:03 2002 +0100
@@ -165,7 +165,7 @@
 We get the following proof state:
 @{subgoals[display,indent=0,margin=65]}
 After stripping the @{text"\<forall>i"}, the proof continues with a case
-distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on
+distinction on @{term"i"}. The case @{prop"i = (0::nat)"} is trivial and we focus on
 the other case:
 *}