doc-src/TutorialI/Misc/natsum.thy

--- a/doc-src/TutorialI/Misc/natsum.thy	Thu Jan 10 01:13:41 2002 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy	Thu Jan 10 11:22:03 2002 +0100
@@ -114,7 +114,7 @@
 
   Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
   role, it may fail to prove a valid formula, for example
-  @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare.
+  @{text"m+m \<noteq> n+n+(1::nat)"}. Fortunately, such examples are rare.
 \end{warn}
 *}