--- 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]