1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 05 18:32:33 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 05 18:32:57 2001 +0100
     1.3 @@ -72,6 +72,7 @@
     1.4  
     1.5  A final alternative is to replace the offending simplification rules by
     1.6  derived conditional ones. For @{term gcd} it means we have to prove
     1.7 +these lemmas:
     1.8  *}
     1.9  
    1.10  lemma [simp]: "gcd (m, 0) = m";
    1.11 @@ -82,7 +83,7 @@
    1.12  done
    1.13  
    1.14  text{*\noindent
    1.15 -after which we can disable the original simplification rule:
    1.16 +Now we can disable the original simplification rule:
    1.17  *}
    1.18  
    1.19  declare gcd.simps [simp del]