--- a/src/HOL/Library/GCD.thy Mon Jul 21 15:26:26 2008 +0200
+++ b/src/HOL/Library/GCD.thy Mon Jul 21 15:27:23 2008 +0200
@@ -163,11 +163,8 @@
text {* \medskip Addition laws *}
-lemma gcd_add1 [simp,algebra]: "gcd (m + n) n = gcd m n"
- apply (case_tac "n = 0")
- apply (simp_all add: gcd_non_0)
- apply (simp add: mod_add_self2)
- done
+lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
+ by (cases "n = 0") (auto simp add: gcd_non_0)
lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
proof -