--- a/NEWS Sun Oct 09 08:30:48 2011 +0200
+++ b/NEWS Sun Oct 09 11:13:53 2011 +0200
@@ -4,6 +4,45 @@
New in this Isabelle version
----------------------------
+*** HOL ***
+
+* Theory Int: Discontinued many legacy theorems specific to type int.
+ INCOMPATIBILITY, use the corresponding generic theorems instead.
+
+ zminus_zminus ~> minus_minus
+ zminus_0 ~> minus_zero
+ zminus_zadd_distrib ~> minus_add_distrib
+ zadd_commute ~> add_commute
+ zadd_assoc ~> add_assoc
+ zadd_left_commute ~> add_left_commute
+ zmult_ac ~> mult_ac
+ zadd_0 ~> add_0_left
+ zadd_0_right ~> add_0_right
+ zadd_zminus_inverse2 ~> left_minus
+ zmult_zminus ~> mult_minus_left
+ zmult_commute ~> mult_commute
+ zmult_assoc ~> mult_assoc
+ zadd_zmult_distrib ~> left_distrib
+ zadd_zmult_distrib2 ~> right_distrib
+ zdiff_zmult_distrib ~> left_diff_distrib
+ zdiff_zmult_distrib2 ~> right_diff_distrib
+ zmult_1 ~> mult_1_left
+ zmult_1_right ~> mult_1_right
+ zle_refl ~> order_refl
+ zle_trans ~> order_trans
+ zle_antisym ~> order_antisym
+ zle_linear ~> linorder_linear
+ zless_linear ~> linorder_less_linear
+ zadd_left_mono ~> add_left_mono
+ zadd_strict_right_mono ~> add_strict_right_mono
+ zadd_zless_mono ~> add_less_le_mono
+ int_0_less_1 ~> zero_less_one
+ int_0_neq_1 ~> zero_neq_one
+ zless_le ~> less_le
+ zpower_zadd_distrib ~> power_add
+ zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
+ zero_le_zpower_abs ~> zero_le_power_abs
+
New in Isabelle2011-1 (October 2011)
--- a/src/HOL/Int.thy Sun Oct 09 08:30:48 2011 +0200
+++ b/src/HOL/Int.thy Sun Oct 09 11:13:53 2011 +0200
@@ -2431,40 +2431,8 @@
subsection {* Legacy theorems *}
-lemmas zminus_zminus = minus_minus [of "z::int", standard]
-lemmas zminus_0 = minus_zero [where 'a=int]
-lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
-lemmas zadd_commute = add_commute [of "z::int" "w", standard]
-lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
-lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
-lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
-lemmas zmult_ac = mult_ac
-lemmas zadd_0 = add_0_left [of "z::int", standard]
-lemmas zadd_0_right = add_0_right [of "z::int", standard]
-lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
-lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
-lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
-lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
-lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
-lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
-lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
-lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
-
-lemmas zmult_1 = mult_1_left [of "z::int", standard]
-lemmas zmult_1_right = mult_1_right [of "z::int", standard]
-
-lemmas zle_refl = order_refl [of "w::int", standard]
-lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
-lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
-lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
-lemmas zless_linear = linorder_less_linear [where 'a = int]
-
-lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
-lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
-lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
-
-lemmas int_0_less_1 = zero_less_one [where 'a=int]
-lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
+(* used by Tools/Qelim/cooper.ML *)
+lemmas zadd_ac = add_ac [where 'a=int]
lemmas inj_int = inj_of_nat [where 'a=int]
lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
@@ -2482,19 +2450,6 @@
lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
-lemmas zless_le = less_int_def
-lemmas int_eq_of_nat = TrueI
-
-lemma zpower_zadd_distrib:
- "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
- by (rule power_add)
-
-lemma zero_less_zpower_abs_iff:
- "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
- by (rule zero_less_power_abs_iff)
-
-lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
- by (rule zero_le_power_abs)
lemma zpower_zpower:
"(x ^ y) ^ z = (x ^ (y * z)::int)"