--- a/src/HOL/Divides.thy Mon Jul 21 15:26:26 2008 +0200
+++ b/src/HOL/Divides.thy Mon Jul 21 15:27:23 2008 +0200
@@ -98,21 +98,21 @@
lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
using div_mult_self2_is_id [of _ 1] by simp
-lemma div_add_self1:
+lemma div_add_self1 [simp]:
assumes "b \<noteq> 0"
shows "(b + a) div b = a div b + 1"
using assms div_mult_self1 [of b a 1] by (simp add: add_commute)
-lemma div_add_self2:
+lemma div_add_self2 [simp]:
assumes "b \<noteq> 0"
shows "(a + b) div b = a div b + 1"
using assms div_add_self1 [of b a] by (simp add: add_commute)
-lemma mod_add_self1:
+lemma mod_add_self1 [simp]:
"(b + a) mod b = a mod b"
using mod_mult_self1 [of a 1 b] by (simp add: add_commute)
-lemma mod_add_self2:
+lemma mod_add_self2 [simp]:
"(a + b) mod b = a mod b"
using mod_mult_self1 [of a 1 b] by simp
--- a/src/HOL/HoareParallel/RG_Examples.thy Mon Jul 21 15:26:26 2008 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Mon Jul 21 15:27:23 2008 +0200
@@ -293,7 +293,7 @@
apply force
apply force
apply(rule Basic)
- apply (simp add: mod_add_self2)
+ apply simp
apply clarify
apply simp
apply (case_tac "X x (j mod n) \<le> j")
@@ -346,7 +346,7 @@
apply(rule Basic)
apply simp
apply clarify
- apply (simp add: mod_add_self2)
+ apply simp
apply(rule allI)
apply(rule impI)+
apply(case_tac "X x ! i\<le> j")
--- 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 -