diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -72,6 +72,7 @@
 
 A final alternative is to replace the offending simplification rules by
 derived conditional ones. For @{term gcd} it means we have to prove
+these lemmas:
 *}
 
 lemma [simp]: "gcd (m, 0) = m";
@@ -82,7 +83,7 @@
 done
 
 text{*\noindent
-after which we can disable the original simplification rule:
+Now we can disable the original simplification rule:
 *}
 
 declare gcd.simps [simp del]