--- 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:
*}