diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -105,7 +105,7 @@
 @{thm[display]nat0_intermed_int_val[no_vars]}
 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
 @{term abs} is the absolute value function, and @{term"#1::int"} is the
-integer 1 (see \S\ref{sec:int}).
+integer 1 (see \S\ref{sec:numbers}).
 
 First we show that the our specific function, the difference between the
 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
@@ -120,7 +120,7 @@
        int(size[x\<in>take (i+1) w. \<not>P x]))
       -
       (int(size[x\<in>take i w.  P x]) -
-       int(size[x\<in>take i w. \<not>P x]))) <= #1";
+       int(size[x\<in>take i w. \<not>P x]))) \<le> #1";
 
 txt{*\noindent
 The lemma is a bit hard to read because of the coercion function