equal
deleted
inserted
replaced
88 A final alternative is to replace the offending simplification rules by |
88 A final alternative is to replace the offending simplification rules by |
89 derived conditional ones. For \isa{gcd} it means we have to prove |
89 derived conditional ones. For \isa{gcd} it means we have to prove |
90 *} |
90 *} |
91 |
91 |
92 lemma [simp]: "gcd (m, 0) = m"; |
92 lemma [simp]: "gcd (m, 0) = m"; |
93 apply(simp).; |
93 by(simp); |
94 lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"; |
94 lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"; |
95 apply(simp).; |
95 by(simp); |
96 |
96 |
97 text{*\noindent |
97 text{*\noindent |
98 after which we can disable the original simplification rule: |
98 after which we can disable the original simplification rule: |
99 *} |
99 *} |
100 |
100 |