diff -r cb0021d56e11 -r 55676111ed69 src/HOL/Library/GCD.thy
--- 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 -