diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -75,7 +75,8 @@
 In fact, this is probably the neatest solution next to pattern matching.
 
 A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove%
+derived conditional ones. For \isa{gcd} it means we have to prove
+these lemmas:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
@@ -85,7 +86,7 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
-after which we can disable the original simplification rule:%
+Now we can disable the original simplification rule:%
 \end{isamarkuptext}%
 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
 \end{isabellebody}%