doc-src/TutorialI/Recdef/simplification.thy

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