# HG changeset patch
# User haftmann
# Date 1279548584 -7200
# Node ID 2ae085b07f2fb9bc14a9dac83309f5405c3ed351
# Parent  2f9d3fc1a8ac341361f2fa38f4f3cd68209e16d9
diff_minus subsumes diff_def

diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Complex.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -686,12 +686,12 @@
 by (simp add: divide_inverse rcis_def)
 
 lemma cis_divide: "cis a / cis b = cis (a - b)"
-by (simp add: complex_divide_def cis_mult diff_def)
+by (simp add: complex_divide_def cis_mult diff_minus)
 
 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
 apply (simp add: complex_divide_def)
 apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_def)
+apply (simp add: rcis_inverse rcis_mult diff_minus)
 done
 
 lemma Re_cis [simp]: "Re(cis a) = cos a"
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -18,7 +18,7 @@
   shows "a 0 - x * (\<Sum> i=0..<n. (-1)^i * a (Suc i) * x^i) = (\<Sum> i=0..<Suc n. (-1)^i * a i * x^i)"
 proof -
   have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
-  show ?thesis unfolding setsum_right_distrib shift_pow diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
+  show ?thesis unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
     setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
 qed
 
@@ -45,14 +45,14 @@
   case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
 next
   case (Suc n)
-  have "?lb (Suc n) j' \<le> ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_def
+  have "?lb (Suc n) j' \<le> ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_minus
   proof (rule add_mono)
     show "real (lapprox_rat prec 1 (int (f j'))) \<le> 1 / real (f j')" using lapprox_rat[of prec 1  "int (f j')"] by auto
     from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> real x`
     show "- real (x * ub n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x) \<le> - (real x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (real x))"
       unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono)
   qed
-  moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_def
+  moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_minus
   proof (rule add_mono)
     show "1 / real (f j') \<le> real (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
     from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> real x`
@@ -1213,7 +1213,7 @@
           round_down[of prec "lb_pi prec"] by auto
   hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
     using x by (cases "k = 0") (auto intro!: add_mono
-                simp add: diff_def k[symmetric] less_float_def)
+                simp add: diff_minus k[symmetric] less_float_def)
   note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
   hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
 
@@ -1227,7 +1227,7 @@
     also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
       using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
       by (simp only: real_of_float_minus real_of_int_minus
-        cos_minus diff_def mult_minus_left)
+        cos_minus diff_minus mult_minus_left)
     finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
       unfolding cos_periodic_int . }
   note negative_lx = this
@@ -1240,7 +1240,7 @@
     have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
       using cos_monotone_0_pi'[OF lx_0 lx pi_x]
       by (simp only: real_of_float_minus real_of_int_minus
-        cos_minus diff_def mult_minus_left)
+        cos_minus diff_minus mult_minus_left)
     also have "\<dots> \<le> real (ub_cos prec ?lx)"
       using lb_cos[OF lx_0 pi_lx] by simp
     finally have "cos x \<le> real (ub_cos prec ?lx)"
@@ -1255,7 +1255,7 @@
     have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
       using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
       by (simp only: real_of_float_minus real_of_int_minus
-          cos_minus diff_def mult_minus_left)
+          cos_minus diff_minus mult_minus_left)
     also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
       using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
     finally have "cos x \<le> real (ub_cos prec (- ?ux))"
@@ -1272,7 +1272,7 @@
     also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
       using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
       by (simp only: real_of_float_minus real_of_int_minus
-        cos_minus diff_def mult_minus_left)
+        cos_minus diff_minus mult_minus_left)
     finally have "real (lb_cos prec ?ux) \<le> cos x"
       unfolding cos_periodic_int . }
   note positive_ux = this
@@ -1347,7 +1347,7 @@
       also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
         using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
         by (simp only: real_of_float_minus real_of_int_minus real_of_one
-            number_of_Min diff_def mult_minus_left mult_1_left)
+            number_of_Min diff_minus mult_minus_left mult_1_left)
       also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
         unfolding real_of_float_minus cos_minus ..
       also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1391,7 +1391,7 @@
       also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
         using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
         by (simp only: real_of_float_minus real_of_int_minus real_of_one
-          number_of_Min diff_def mult_minus_left mult_1_left)
+          number_of_Min diff_minus mult_minus_left mult_1_left)
       also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
         using lb_cos[OF lx_0 pi_lx] by simp
       finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -2091,12 +2091,12 @@
   unfolding divide_inverse interpret_floatarith.simps ..
 
 lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
-  unfolding diff_def interpret_floatarith.simps ..
+  unfolding diff_minus interpret_floatarith.simps ..
 
 lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   sin (interpret_floatarith a vs)"
   unfolding sin_cos_eq interpret_floatarith.simps
-            interpret_floatarith_divide interpret_floatarith_diff diff_def
+            interpret_floatarith_divide interpret_floatarith_diff diff_minus
   by auto
 
 lemma interpret_floatarith_tan:
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -1356,7 +1356,7 @@
     also have "\<dots> = (j dvd (- (c*x - ?e)))"
     by (simp only: dvd_minus_iff)
   also have "\<dots> = (j dvd (c* (- x)) + ?e)"
-    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
+    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
     by (simp add: algebra_simps)
   also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
@@ -1368,7 +1368,7 @@
     also have "\<dots> = (j dvd (- (c*x - ?e)))"
     by (simp only: dvd_minus_iff)
   also have "\<dots> = (j dvd (c* (- x)) + ?e)"
-    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
+    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
     by (simp add: algebra_simps)
   also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -1768,7 +1768,7 @@
   have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
   show ?thesis using myless[rule_format, where b="real (floor b)"] 
     by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) 
-    (simp add: algebra_simps diff_def[symmetric],arith)
+    (simp add: algebra_simps diff_minus[symmetric],arith)
 qed
 
 lemma split_int_le_real: 
@@ -1795,7 +1795,7 @@
 proof- 
   have th: "(real a + b \<ge>0) = (real (-a) + (-b) \<le> 0)" by arith
   show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
-    (simp add: algebra_simps diff_def[symmetric],arith)
+    (simp add: algebra_simps diff_minus[symmetric],arith)
 qed
 
 lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \<and> b = real (floor b))" (is "?l = ?r")
@@ -1828,13 +1828,13 @@
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def diff_def)
+    also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def diff_minus)
     finally have ?case using l by simp}
   moreover
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1853,13 +1853,13 @@
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_def)
+    also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
     finally have ?case using l by simp}
   moreover
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac ,arith)
+    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac ,arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1878,13 +1878,13 @@
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_def)
+    also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
     finally have ?case using l by simp}
   moreover
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1903,13 +1903,13 @@
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_def)
+    also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
     finally have ?case using l by simp}
   moreover
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -3337,7 +3337,7 @@
     hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
     with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1" 
-      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
+      by (simp only: diff_minus[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
     with nob  have ?case by blast }
   ultimately show ?case by blast
 next
@@ -3360,11 +3360,11 @@
     hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
     with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
-      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) 
+      by (simp only: diff_minus[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) 
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
-      by (simp only: algebra_simps diff_def[symmetric])
+      by (simp only: algebra_simps diff_minus[symmetric])
         hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
-          by (simp only: add_ac diff_def)
+          by (simp only: add_ac diff_minus)
     with nob  have ?case by blast }
   ultimately show ?case by blast
 next
@@ -3822,7 +3822,7 @@
       by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"]) 
     hence "\<exists> j\<in> {n .. 0}. 0 \<ge> - (real n *x + ?N s - ?N (Floor s) - real j) \<and> - (real n *x + ?N s - ?N (Floor s) - real (j+1)) > 0" by (simp only: th1[rule_format] th2[rule_format])
     hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
-      using pns by (simp add: fp_def nn diff_def add_ac mult_ac numfloor numadd numneg
+      using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
         del: diff_less_0_iff_less diff_le_0_iff_le) 
     then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
     hence "\<exists>x \<in> {?p (p,n,s) j |j. n\<le> j \<and> j \<le> 0 }. ?I x" by auto
@@ -4036,7 +4036,7 @@
   from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
     by (simp add: iupt_set np DVDJ_def del: iupt.simps)
-  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_def[symmetric])
+  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_minus[symmetric])
   also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
   finally show ?thesis by simp
@@ -4051,7 +4051,7 @@
   from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
     by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
-  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_def[symmetric])
+  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_minus[symmetric])
   also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
   finally show ?thesis by simp
@@ -5093,7 +5093,7 @@
   shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
 proof-
   have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
-    by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_def)
+    by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_minus)
   also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
     by (simp only: exsplit[OF qf] add_ac)
   also have "\<dots> = (\<exists> x. Ifm (x#bs) p)" 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Jul 19 16:09:44 2010 +0200
@@ -36,7 +36,7 @@
              @{thm "divide_zero"}, 
              @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
              @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
-             @{thm "diff_def"}, @{thm "minus_divide_left"}]
+             @{thm "diff_minus"}, @{thm "minus_divide_left"}]
 val comp_ths = ths @ comp_arith @ simp_thms 
 
 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Deriv.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -57,7 +57,7 @@
 
 lemma DERIV_diff:
   "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
-by (simp only: diff_def DERIV_add DERIV_minus)
+by (simp only: diff_minus DERIV_add DERIV_minus)
 
 lemma DERIV_add_minus:
   "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
@@ -1269,7 +1269,7 @@
       and "f b - f a = (b - a) * l"
     by auto
   from prems have "~(l >= 0)"
-    by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
+    by (metis diff_self diff_eq_diff_less_eq' le_iff_diff_le_0 order_antisym linear
               split_mult_pos_le)
   with prems show False
     by (metis DERIV_unique order_less_imp_le)
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -118,7 +118,7 @@
 proof -
   assume x: "x \<in> V"
   have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
-    by (simp add: diff_def)
+    by (simp add: diff_minus)
   also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
     by (rule add_mult_distrib2)
   also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Import/HOL/poly.imp
--- a/src/HOL/Import/HOL/poly.imp	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Import/HOL/poly.imp	Mon Jul 19 16:09:44 2010 +0200
@@ -13,7 +13,7 @@
   "poly_add" > "poly_add_primdef"
   "poly" > "poly_primdef"
   "normalize" > "normalize_def"
-  "diff" > "diff_def"
+  "diff" > "diff_minus"
   "degree" > "degree_def"
   "##" > "##_def"
 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Import/HOL/real.imp	Mon Jul 19 16:09:44 2010 +0200
@@ -25,7 +25,7 @@
   "sumc" > "HOL4Real.real.sumc"
   "sum_def" > "HOL4Real.real.sum_def"
   "sum" > "HOL4Real.real.sum"
-  "real_sub" > "Groups.diff_def"
+  "real_sub" > "Groups.diff_minus"
   "real_of_num" > "HOL4Compat.real_of_num"
   "real_lte" > "HOL4Compat.real_lte"
   "real_lt" > "Orderings.linorder_not_le"
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Int.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -566,7 +566,7 @@
   obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
 apply (cases z rule: eq_Abs_Integ)
 apply (rule_tac m=x and n=y in diff)
-apply (simp add: int_def diff_def minus add)
+apply (simp add: int_def minus add diff_minus)
 done
 
 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -221,12 +221,12 @@
     from unimodular_reduce_norm[OF th0] o
     have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
       apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
-      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
+      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
       apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
       apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
       apply (rule_tac x="- ii" in exI, simp add: m power_mult)
-      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
-      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
+      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
+      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
       done
     then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
     let ?w = "v / complex_of_real (root n (cmod b))"
@@ -959,7 +959,7 @@
 
 lemma mpoly_sub_conv:
   "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
-  by (simp add: diff_def)
+  by (simp add: diff_minus)
 
 lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -204,7 +204,7 @@
     from Cons.hyps[rule_format, of x]
     obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
     have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
-      using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric]
+      using qr by(cases q, simp_all add: algebra_simps diff_minus[symmetric]
         minus_mult_left[symmetric] right_minus)
     hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
   thus ?case by blast
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -523,7 +523,7 @@
 lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
 
 lemma linear_sub: "linear f ==> f(x - y) = f x - f y"
-  by (simp add: diff_def linear_add linear_neg)
+  by (simp add: diff_minus linear_add linear_neg)
 
 lemma linear_setsum:
   assumes lf: "linear f" and fS: "finite S"
@@ -592,10 +592,10 @@
     by (simp add: eq_add_iff field_simps)
 
 lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z"
-  by (simp  add: diff_def bilinear_ladd bilinear_lneg)
+  by (simp  add: diff_minus bilinear_ladd bilinear_lneg)
 
 lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y"
-  by (simp  add: diff_def bilinear_radd bilinear_rneg)
+  by (simp  add: diff_minus bilinear_radd bilinear_rneg)
 
 lemma bilinear_setsum:
   assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"
@@ -902,7 +902,7 @@
   by (metis scaleR_minus1_left subspace_mul)
 
 lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
-  by (metis diff_def subspace_add subspace_neg)
+  by (metis diff_minus subspace_add subspace_neg)
 
 lemma (in real_vector) subspace_setsum:
   assumes sA: "subspace A" and fB: "finite B"
@@ -3082,7 +3082,7 @@
   from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
   have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
     "infnorm y \<le> infnorm (x - y) + infnorm x"
-    by (simp_all add: field_simps infnorm_neg diff_def[symmetric])
+    by (simp_all add: field_simps infnorm_neg diff_minus[symmetric])
   from th[OF ths]  show ?thesis .
 qed
 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -174,7 +174,7 @@
 apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
 apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
 apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
-apply (auto simp add: diff_def add_ac)
+apply (auto simp add: diff_minus add_ac)
 done
 
 text{*Product of functions - Proof is trivial but tedious
@@ -234,7 +234,7 @@
   hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
     by (rule NSLIM_minus)
   have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
-    by (simp add: minus_divide_left diff_def)
+    by (simp add: minus_divide_left diff_minus)
   with deriv
   show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
 qed
@@ -353,7 +353,7 @@
 (*apply (auto simp add: starfun_inverse_inverse realpow_two
         simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*)
 apply (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric] power_Suc
-              nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_def
+              nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus
             del: inverse_mult_distrib inverse_minus_eq
                  minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/HLim.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -73,7 +73,7 @@
 
 lemma NSLIM_diff:
   "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
-by (simp only: diff_def NSLIM_add NSLIM_minus)
+by (simp only: diff_minus NSLIM_add NSLIM_minus)
 
 lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
 by (simp only: NSLIM_add NSLIM_minus)
@@ -245,7 +245,7 @@
 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
 apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
 apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
- prefer 2 apply (simp add: add_commute diff_def [symmetric])
+ prefer 2 apply (simp add: add_commute diff_minus [symmetric])
 apply (rule_tac x = x in star_cases)
 apply (rule_tac [2] x = x in star_cases)
 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/HTranscendental.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -258,7 +258,7 @@
             simp add: mult_assoc)
 apply (rule approx_add_right_cancel [where d="-1"])
 apply (rule approx_sym [THEN [2] approx_trans2])
-apply (auto simp add: diff_def mem_infmal_iff)
+apply (auto simp add: diff_minus mem_infmal_iff)
 done
 
 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
@@ -450,7 +450,7 @@
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
             simp add: mult_assoc)
 apply (rule approx_add_right_cancel [where d = "-1"])
-apply (simp add: diff_def)
+apply (simp add: diff_minus)
 done
 
 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/NSA.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -368,7 +368,7 @@
 
 lemma Infinitesimal_diff:
      "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
-by (simp add: diff_def Infinitesimal_add)
+by (simp add: diff_minus Infinitesimal_add)
 
 lemma Infinitesimal_mult:
   fixes x y :: "'a::real_normed_algebra star"
@@ -637,7 +637,7 @@
 lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
 apply (simp add: approx_def)
 apply (drule (1) Infinitesimal_add)
-apply (simp add: diff_def)
+apply (simp add: diff_minus)
 done
 
 lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
@@ -714,7 +714,7 @@
 lemma approx_minus: "a @= b ==> -a @= -b"
 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
 apply (drule approx_minus_iff [THEN iffD1])
-apply (simp add: add_commute diff_def)
+apply (simp add: add_commute diff_minus)
 done
 
 lemma approx_minus2: "-a @= -b ==> a @= b"
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/NSA/NSCA.thy
--- a/src/HOL/NSA/NSCA.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -178,7 +178,7 @@
      "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
 apply (drule approx_approx_zero_iff [THEN iffD1])
 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
-apply (auto simp add: mem_infmal_iff [symmetric] diff_def)
+apply (auto simp add: mem_infmal_iff [symmetric] diff_minus)
 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
 apply (auto simp add: diff_minus [symmetric])
 done
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -357,7 +357,7 @@
                     borel_measurable_uminus_borel_measurable f g)
   finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
   show ?thesis
-    apply (simp add: times_eq_sum_squares diff_def) 
+    apply (simp add: times_eq_sum_squares diff_minus) 
     using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
     done
 qed
@@ -366,7 +366,7 @@
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-unfolding diff_def
+unfolding diff_minus
   by (fast intro: borel_measurable_add_borel_measurable 
                   borel_measurable_uminus_borel_measurable f g)
 
@@ -626,11 +626,11 @@
 proof -
   from assms have "y - z > 0" by simp
   hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
-    unfolding incseq_def LIMSEQ_def dist_real_def diff_def
+    unfolding incseq_def LIMSEQ_def dist_real_def diff_minus
     by simp
   have "\<forall>m. x m \<le> y" using incseq_le assms by auto
   hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
-    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_def)
+    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_minus)
   from A B show ?thesis by auto
 qed
 
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/RComplete.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -153,7 +153,7 @@
   have "x = y-(y-x)" by simp
   also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
   also have "\<dots> = real p / real q"
-    by (simp only: inverse_eq_divide diff_def real_of_nat_Suc 
+    by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc 
     minus_divide_left add_divide_distrib[THEN sym]) simp
   finally have "x<r" by (unfold r_def)
   have "p<Suc p" .. also note main[THEN sym]
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/RealVector.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -30,7 +30,7 @@
 qed
 
 lemma diff: "f (x - y) = f x - f y"
-by (simp add: diff_def add minus)
+by (simp add: add minus diff_minus)
 
 lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
 apply (cases "finite A")
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/SEQ.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -506,8 +506,7 @@
       from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
         by blast
       thus "lim f \<le> x"
-        by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
-                  linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) 
+        by (metis 1 LIMSEQ_le_const2 fn_le)
     qed
 qed
 
@@ -971,7 +970,7 @@
 apply (rule_tac x = K in exI, simp)
 apply (rule exI [where x = 0], auto)
 apply (erule order_less_le_trans, simp)
-apply (drule_tac x=n in spec, fold diff_def)
+apply (drule_tac x=n in spec, fold diff_minus)
 apply (drule order_trans [OF norm_triangle_ineq2])
 apply simp
 done
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -417,7 +417,7 @@
   also have "... \<le> e" 
     apply (rule Sup_asclose) 
     apply (auto simp add: S)
-    apply (metis abs_minus_add_cancel b add_commute diff_def)
+    apply (metis abs_minus_add_cancel b add_commute diff_minus)
     done
   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   thus ?thesis
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 19 16:09:44 2010 +0200
@@ -734,7 +734,7 @@
            @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
            @{thm "times_divide_times_eq"},
            @{thm "divide_divide_eq_right"},
-           @{thm "diff_def"}, @{thm "minus_divide_left"},
+           @{thm "diff_minus"}, @{thm "minus_divide_left"},
            @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
            @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
            Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Transcendental.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -2952,7 +2952,7 @@
       }
       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
-        unfolding diff_def divide_inverse
+        unfolding diff_minus divide_inverse
         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
       ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
       hence "?diff 1 n \<le> ?a 1 n" by auto
@@ -2968,7 +2968,7 @@
         have "norm (?diff 1 n - 0) < r" by auto }
       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
     qed
-    from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
+    from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
     
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -292,7 +292,7 @@
 
 (* two alternative proofs of this *)
 lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
-  apply (unfold diff_def)
+  apply (unfold diff_minus)
   apply (rule mem_same)
    apply (rule RI_minus RI_add RI_int)+
   apply simp
diff -r 2f9d3fc1a8ac -r 2ae085b07f2f src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Word/Word.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -1130,14 +1130,14 @@
 lemmas wi_hom_syms = wi_homs [symmetric]
 
 lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
-  unfolding word_sub_wi diff_def
+  unfolding word_sub_wi diff_minus
   by (simp only : word_uint.Rep_inverse wi_hom_syms)
     
 lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
 
 lemma word_of_int_sub_hom:
   "(word_of_int a) - word_of_int b = word_of_int (a - b)"
-  unfolding word_sub_def diff_def by (simp only : wi_homs)
+  unfolding word_sub_def diff_minus by (simp only : wi_homs)
 
 lemmas new_word_of_int_homs = 
   word_of_int_sub_hom wi_homs word_0_wi word_1_wi