1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Jul 28 13:04:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Jul 28 16:02:51 2000 +0200
     1.3 @@ -90,9 +90,9 @@
     1.4  *}
     1.5  
     1.6  lemma [simp]: "gcd (m, 0) = m";
     1.7 -apply(simp).;
     1.8 +by(simp);
     1.9  lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
    1.10 -apply(simp).;
    1.11 +by(simp);
    1.12  
    1.13  text{*\noindent
    1.14  after which we can disable the original simplification rule: