diff -r 042015819774 -r 603df40ef1e9 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Feb 16 13:47:06 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Feb 16 18:50:09 2001 +0100
@@ -1085,17 +1085,16 @@
 A more challenging example illustrates how Isabelle/HOL defines the least-number
 operator, which denotes the least \isa{x} satisfying~\isa{P}:
 \begin{isabelle}
-(LEAST\ x.\ P\ x)\ \isasymequiv \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
+(LEAST\ x.\ P\ x)\ = \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
 P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)
-\rulename{Least_def}
 \end{isabelle}
 
 Let us prove the counterpart of \isa{some_equality} for this operator.
-The first step merely unfolds the definition:
+The first step merely unfolds the definitions:
 \begin{isabelle}
 \isacommand{theorem}\ Least_equality:\isanewline
 \ \ \ \ \ "\isasymlbrakk \ P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\ \isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
-\isacommand{apply}\ (simp\ add:\ Least_def)\isanewline
+\isacommand{apply}\ (simp\ add:\ Least_def\ LeastM_def)\isanewline
 %\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
 %\isasymle \ x\isasymrbrakk \isanewline
 %\ \ \ \ \isasymLongrightarrow \ (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%