--- a/src/HOL/Integration.thy Sat Feb 07 10:56:44 2009 +0100
+++ b/src/HOL/Integration.thy Sun Feb 08 11:59:26 2009 +0100
@@ -558,7 +558,7 @@
apply (frule partition_eq_bound)
apply (drule_tac [2] partition_gt, auto)
apply (metis linear not_less partition_rhs partition_rhs2)
-apply (metis add_diff_inverse diff_is_0_eq le0 le_diff_conv nat_add_commute partition partition_eq_bound partition_rhs real_less_def termination_basic_simps(5))
+apply (metis lemma_additivity1 order_less_trans partition_eq_bound partition_lb partition_rhs)
done
lemma lemma_additivity4_psize_eq:
--- a/src/HOL/OrderedGroup.thy Sat Feb 07 10:56:44 2009 +0100
+++ b/src/HOL/OrderedGroup.thy Sun Feb 08 11:59:26 2009 +0100
@@ -598,12 +598,12 @@
by (simp add: algebra_simps)
text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps = algebra_simps
+lemmas group_simps[noatp] = algebra_simps
end
text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps = algebra_simps
+lemmas group_simps[noatp] = algebra_simps
class ordered_ab_semigroup_add =
linorder + pordered_ab_semigroup_add
@@ -1310,9 +1310,9 @@
add_less_le_mono add_le_less_mono add_strict_mono)
text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
+lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
-lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
+lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
ML {*
structure ab_group_add_cancel = Abel_Cancel
--- a/src/HOL/Ring_and_Field.thy Sat Feb 07 10:56:44 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Sun Feb 08 11:59:26 2009 +0100
@@ -232,8 +232,8 @@
by (rule equals_zero_I) (simp add: right_distrib [symmetric])
text{*Extract signs from products*}
-lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
lemma minus_mult_minus [simp]: "- a * - b = a * b"
by simp
@@ -247,11 +247,11 @@
lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
by (simp add: left_distrib diff_minus)
-lemmas ring_distribs =
+lemmas ring_distribs[noatp] =
right_distrib left_distrib left_diff_distrib right_diff_distrib
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
lemma eq_add_iff1:
"a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -263,7 +263,7 @@
end
-lemmas ring_distribs =
+lemmas ring_distribs[noatp] =
right_distrib left_distrib left_diff_distrib right_diff_distrib
class comm_ring = comm_semiring + ab_group_add
@@ -751,7 +751,7 @@
subclass pordered_ab_group_add ..
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
lemma less_add_iff1:
"a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
@@ -960,7 +960,7 @@
end
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
class pordered_comm_ring = comm_ring + pordered_comm_semiring
@@ -1107,7 +1107,7 @@
text {* Simprules for comparisons where common factors can be cancelled. *}
-lemmas mult_compare_simps =
+lemmas mult_compare_simps[noatp] =
mult_le_cancel_right mult_le_cancel_left
mult_le_cancel_right1 mult_le_cancel_right2
mult_le_cancel_left1 mult_le_cancel_left2
@@ -1219,7 +1219,7 @@
lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
by (simp add: divide_inverse mult_ac)
-lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
lemma divide_divide_eq_right [simp,noatp]:
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
@@ -1297,8 +1297,8 @@
text{*The effect is to extract signs from divisions*}
-lemmas divide_minus_left = minus_divide_left [symmetric]
-lemmas divide_minus_right = minus_divide_right [symmetric]
+lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
+lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
declare divide_minus_left [simp] divide_minus_right [simp]
lemma minus_divide_divide [simp]:
@@ -1359,7 +1359,7 @@
by (subst eq_divide_eq, simp)
-lemmas field_eq_simps = algebra_simps
+lemmas field_eq_simps[noatp] = algebra_simps
(* pull / out*)
add_divide_eq_iff divide_add_eq_iff
diff_divide_eq_iff divide_diff_eq_iff
@@ -1720,7 +1720,7 @@
(for inequations). Can be too aggressive and is therefore separate from the
more benign @{text algebra_simps}. *}
-lemmas field_simps = field_eq_simps
+lemmas field_simps[noatp] = field_eq_simps
(* multiply ineqn *)
pos_divide_less_eq neg_divide_less_eq
pos_less_divide_eq neg_less_divide_eq
@@ -1732,7 +1732,7 @@
sign_simps} to @{text field_simps} because the former can lead to case
explosions. *}
-lemmas sign_simps = group_simps
+lemmas sign_simps[noatp] = group_simps
zero_less_mult_iff mult_less_0_iff
(* Only works once linear arithmetic is installed:
@@ -1856,9 +1856,9 @@
lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
-declare zero_less_divide_1_iff [simp]
+declare zero_less_divide_1_iff [simp,noatp]
declare divide_less_0_1_iff [simp,noatp]
-declare zero_le_divide_1_iff [simp]
+declare zero_le_divide_1_iff [simp,noatp]
declare divide_le_0_1_iff [simp,noatp]
@@ -2234,7 +2234,7 @@
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
-lemmas eq_minus_self_iff = equal_neg_zero
+lemmas eq_minus_self_iff[noatp] = equal_neg_zero
lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..