# HG changeset patch
# User wenzelm
# Date 1279723842 -7200
# Node ID eb89d0ac75fb343f3a9c43e3c08fda4819b66999
# Parent  c5ad6fec34701501898b945d696d69b27adea498# Parent  496d723516e627977cb9e81771f59dc415f7efb1
merged

diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Complex.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Deriv.thy	Wed Jul 21 16:50:42 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"
@@ -1255,8 +1255,9 @@
   assume "~ f a \<le> f b"
   assume "a = b"
   with prems show False by auto
-  next assume "~ f a \<le> f b"
-  assume "a ~= b"
+next
+  assume A: "~ f a \<le> f b"
+  assume B: "a ~= b"
   with assms have "EX l z. a < z & z < b & DERIV f z :> l
       & f b - f a = (b - a) * l"
     apply -
@@ -1266,11 +1267,11 @@
      apply (metis differentiableI less_le)
     done
   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
-      and "f b - f a = (b - a) * l"
+      and C: "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
-              split_mult_pos_le)
+  with A have "a < b" "f b < f a" by auto
+  with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
+    (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
   with prems show False
     by (metis DERIV_unique order_less_imp_le)
 qed
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Groups.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -6,7 +6,7 @@
 
 theory Groups
 imports Orderings
-uses ("~~/src/Provers/Arith/abel_cancel.ML")
+uses ("~~/src/HOL/Tools/abel_cancel.ML")
 begin
 
 subsection {* Fact collections *}
@@ -146,8 +146,6 @@
 class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
 
-use "~~/src/Provers/Arith/abel_cancel.ML"
-
 
 subsection {* Semigroups and Monoids *}
 
@@ -453,8 +451,13 @@
 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
 by (simp add: algebra_simps)
 
+lemma diff_eq_diff_eq:
+  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+  by (auto simp add: algebra_simps)
+  
 end
 
+
 subsection {* (Partially) Ordered Groups *} 
 
 text {*
@@ -755,14 +758,16 @@
 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
 by (auto simp add: le_less minus_less_iff)
 
-lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
+lemma diff_less_0_iff_less [simp, no_atp]:
+  "a - b < 0 \<longleftrightarrow> a < b"
 proof -
-  have  "(a < b) = (a + (- b) < b + (-b))"  
-    by (simp only: add_less_cancel_right)
-  also have "... =  (a - b < 0)" by (simp add: diff_minus)
+  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
+  also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   finally show ?thesis .
 qed
 
+lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
+
 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
 apply (subst less_iff_diff_less_0 [of a])
 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
@@ -781,11 +786,32 @@
 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
 
-lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
-by (simp add: algebra_simps)
+lemma diff_le_0_iff_le [simp, no_atp]:
+  "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
+  by (simp add: algebra_simps)
+
+lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
+
+lemma diff_eq_diff_less:
+  "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
+  by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
+
+lemma diff_eq_diff_less_eq:
+  "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
+  by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
 
 end
 
+use "~~/src/HOL/Tools/abel_cancel.ML"
+
+simproc_setup abel_cancel_sum
+  ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
+  {* fn phi => Abel_Cancel.sum_proc *}
+
+simproc_setup abel_cancel_relation
+  ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
+  {* fn phi => Abel_Cancel.rel_proc *}
+
 class linordered_ab_semigroup_add =
   linorder + ordered_ab_semigroup_add
 
@@ -1167,42 +1193,6 @@
 
 end
 
-text {* Needed for abelian cancellation simprocs: *}
-
-lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
-apply (subst add_left_commute)
-apply (subst add_left_cancel)
-apply simp
-done
-
-lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
-apply (subst add_cancel_21[of _ _ _ 0, simplified])
-apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
-done
-
-lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
-by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
-
-lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
-apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
-apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
-done
-
-lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
-
-lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
-by (simp add: diff_minus)
-
-lemma le_add_right_mono: 
-  assumes 
-  "a <= b + (c::'a::ordered_ab_group_add)"
-  "c <= d"    
-  shows "a <= b + d"
-  apply (rule_tac order_trans[where y = "b+c"])
-  apply (simp_all add: prems)
-  done
-
 
 subsection {* Tools setup *}
 
@@ -1224,64 +1214,6 @@
 by (auto intro: add_strict_right_mono add_strict_left_mono
   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, no_atp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
-
-ML {*
-structure ab_group_add_cancel = Abel_Cancel
-(
-
-(* term order for abelian groups *)
-
-fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
-      [@{const_name Groups.zero}, @{const_name Groups.plus},
-        @{const_name Groups.uminus}, @{const_name Groups.minus}]
-  | agrp_ord _ = ~1;
-
-fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
-
-local
-  val ac1 = mk_meta_eq @{thm add_assoc};
-  val ac2 = mk_meta_eq @{thm add_commute};
-  val ac3 = mk_meta_eq @{thm add_left_commute};
-  fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
-        SOME ac1
-    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
-        if termless_agrp (y, x) then SOME ac3 else NONE
-    | solve_add_ac thy _ (_ $ x $ y) =
-        if termless_agrp (y, x) then SOME ac2 else NONE
-    | solve_add_ac thy _ _ = NONE
-in
-  val add_ac_proc = Simplifier.simproc @{theory}
-    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
-end;
-
-val eq_reflection = @{thm eq_reflection};
-  
-val T = @{typ "'a::ab_group_add"};
-
-val cancel_ss = HOL_basic_ss settermless termless_agrp
-  addsimprocs [add_ac_proc] addsimps
-  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
-   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
-   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
-   @{thm minus_add_cancel}];
-
-val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
-  
-val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
-
-val dest_eqI = 
-  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
-
-);
-*}
-
-ML {*
-  Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
-*}
-
 code_modulename SML
   Groups Arith
 
@@ -1291,4 +1223,9 @@
 code_modulename Haskell
   Groups Arith
 
+
+text {* Legacy *}
+
+lemmas diff_def = diff_minus
+
 end
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -1928,7 +1928,7 @@
   (Haskell "True" and "False" and "not"
     and infixl 3 "&&" and infixl 2 "||"
     and "!(if (_)/ then (_)/ else (_))")
-  (Scala "true" and "false" and "'! _"
+  (Scala "true" and "false" and "'!/ _"
     and infixl 3 "&&" and infixl 1 "||"
     and "!(if ((_))/ (_)/ else (_))")
 
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -124,10 +124,10 @@
 *}  
 
 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
-  crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
+  crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
 
 lemma crelI:
-  "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
+  "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
   by (simp add: crel_def)
 
 lemma crelE:
@@ -300,9 +300,9 @@
   using assms by (auto simp add: crel_def bind_def split: option.split_asm)
 
 lemma execute_bind_eq_SomeI:
-  assumes "Heap_Monad.execute f h = Some (x, h')"
-    and "Heap_Monad.execute (g x) h' = Some (y, h'')"
-  shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
+  assumes "execute f h = Some (x, h')"
+    and "execute (g x) h' = Some (y, h'')"
+  shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
   using assms by (simp add: bind_def)
 
 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
@@ -487,7 +487,7 @@
 code_reserved Scala Heap
 
 code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "!Heap.bind((_), (_))")
+code_const bind (Scala "bind")
 code_const return (Scala "('_: Unit)/ =>/ _")
 code_const Heap_Monad.raise' (Scala "!error((_))")
 
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -296,11 +296,11 @@
 
 text {* Scala *}
 
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
+code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
 
 end
 
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -1014,6 +1014,6 @@
 ML {* @{code test_2} () *}
 ML {* @{code test_3} () *}
 
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
 
 end
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Import/HOL/poly.imp
--- a/src/HOL/Import/HOL/poly.imp	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Import/HOL/poly.imp	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Import/HOL/real.imp	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Int.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 21 16:50:42 2010 +0200
@@ -168,6 +168,7 @@
   SAT.thy \
   Set.thy \
   Sum_Type.thy \
+  Tools/abel_cancel.ML \
   Tools/arith_data.ML \
   Tools/cnf_funcs.ML \
   Tools/Datatype/datatype_abs_proofs.ML \
@@ -219,7 +220,6 @@
   Transitive_Closure.thy \
   Typedef.thy \
   Wellfounded.thy \
-  $(SRC)/Provers/Arith/abel_cancel.ML \
   $(SRC)/Provers/Arith/cancel_div_mod.ML \
   $(SRC)/Provers/Arith/cancel_sums.ML \
   $(SRC)/Provers/Arith/fast_lin_arith.ML \
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -312,7 +312,7 @@
   def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
-  def as_Int: Int = if (this.value >= Math.MIN_INT && this.value <= Math.MAX_INT)
+  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
       this.value.intValue
     else this.value.intValue
 
@@ -337,7 +337,7 @@
 
 code_type nat
   (Haskell "Nat.Nat")
-  (Scala "Nat.Nat")
+  (Scala "Nat")
 
 code_instance nat :: eq
   (Haskell -)
@@ -405,7 +405,7 @@
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
-  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
+  (Scala "!_.as'_BigInt" and "Nat")
 
 text {* Conversion from and to indices. *}
 
@@ -419,7 +419,7 @@
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "toEnum")
-  (Scala "!Nat.Nat((_))")
+  (Scala "Nat")
 
 text {* Using target language arithmetic operations whenever appropriate *}
 
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -376,9 +376,10 @@
   "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
 proof -
   assume "a+b <= c"
-  hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
-  have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
-  show ?thesis by (rule le_add_right_mono[OF 2 3])
+  then have "a <= c+(-b)" by (simp add: algebra_simps)
+  have "(-b) <= abs b" by (rule abs_ge_minus_self)
+  then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
+  with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
 qed
 
 class lattice_ring = ordered_ring + lattice_ab_group_add_abs
@@ -411,7 +412,7 @@
     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
     done
   have yx: "?y <= ?x"
-    apply (simp add:diff_def)
+    apply (simp add:diff_minus)
     apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
     apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
     done
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/List.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -4819,7 +4819,7 @@
   (SML "[]")
   (OCaml "[]")
   (Haskell "[]")
-  (Scala "Nil")
+  (Scala "!Nil")
 
 code_instance list :: eq
   (Haskell -)
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Matrix/LP.thy
--- a/src/HOL/Matrix/LP.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Matrix/LP.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -6,6 +6,15 @@
 imports Main Lattice_Algebras
 begin
 
+lemma le_add_right_mono: 
+  assumes 
+  "a <= b + (c::'a::ordered_ab_group_add)"
+  "c <= d"    
+  shows "a <= b + d"
+  apply (rule_tac order_trans[where y = "b+c"])
+  apply (simp_all add: prems)
+  done
+
 lemma linprog_dual_estimate:
   assumes
   "A * x \<le> (b::'a::lattice_ring)"
@@ -49,8 +58,8 @@
     done    
   from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
     by (simp)
-  show ?thesis 
-    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+  show ?thesis
+    apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
     apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
     done
 qed
@@ -138,9 +147,9 @@
   then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
   have s2: "c - y * A <= c2 - y * A1"
-    by (simp add: diff_def prems add_mono mult_left_mono)
+    by (simp add: diff_minus prems add_mono mult_left_mono)
   have s1: "c1 - y * A2 <= c - y * A"
-    by (simp add: diff_def prems add_mono mult_left_mono)
+    by (simp add: diff_minus prems add_mono mult_left_mono)
   have prts: "(c - y * A) * x <= ?C"
     apply (simp add: Let_def)
     apply (rule mult_le_prts)
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/HLim.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/HTranscendental.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/NSA.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/NSA/NSCA.thy
--- a/src/HOL/NSA/NSCA.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -92,7 +92,6 @@
      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
 by (simp add: nat_mult_div_cancel1)
 
-
 use "Tools/numeral_simprocs.ML"
 
 use "Tools/nat_numeral_simprocs.ML"
@@ -117,4 +116,4 @@
   #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
 *}
 
-end
\ No newline at end of file
+end
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Option.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -114,7 +114,7 @@
   (SML "NONE" and "SOME")
   (OCaml "None" and "Some _")
   (Haskell "Nothing" and "Just")
-  (Scala "None" and "!Some((_))")
+  (Scala "!None" and "Some")
 
 code_instance option :: eq
   (Haskell -)
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/RComplete.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/RealVector.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/SEQ.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/SupInf.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Tools/abel_cancel.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/abel_cancel.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -0,0 +1,131 @@
+(*  Title:      HOL/Tools/abel_cancel.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Simplification procedures for abelian groups:
+- Cancel complementary terms in sums.
+- Cancel like terms on opposite sides of relations.
+*)
+
+signature ABEL_CANCEL =
+sig
+  val sum_proc: simpset -> cterm -> thm option
+  val rel_proc: simpset -> cterm -> thm option
+end;
+
+structure Abel_Cancel: ABEL_CANCEL =
+struct
+
+(** compute cancellation **)
+
+fun add_atoms pos (Const (@{const_name Groups.plus}, _) $ x $ y) =
+      add_atoms pos x #> add_atoms pos y
+  | add_atoms pos (Const (@{const_name Groups.minus}, _) $ x $ y) =
+      add_atoms pos x #> add_atoms (not pos) y
+  | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
+      add_atoms (not pos) x
+  | add_atoms pos x = cons (pos, x);
+
+fun atoms t = add_atoms true t [];
+
+fun zerofy pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) =
+      (case zerofy pt x of NONE =>
+        (case zerofy pt y of NONE => NONE
+         | SOME z => SOME (c $ x $ z))
+       | SOME z => SOME (c $ z $ y))
+  | zerofy pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) =
+      (case zerofy pt x of NONE =>
+        (case zerofy (apfst not pt) y of NONE => NONE
+         | SOME z => SOME (c $ x $ z))
+       | SOME z => SOME (c $ z $ y))
+  | zerofy pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) =
+      (case zerofy (apfst not pt) x of NONE => NONE
+       | SOME z => SOME (c $ z))
+  | zerofy (pos, t) u =
+      if pos andalso (t aconv u)
+        then SOME (Const (@{const_name Groups.zero}, fastype_of t))
+        else NONE
+
+exception Cancel;
+
+fun find_common _ [] _ = raise Cancel
+  | find_common opp ((p, l) :: ls) rs =
+      let val pr = if opp then not p else p
+      in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l)
+         else find_common opp ls rs
+      end
+
+(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
+   If OP = +, it must be t2(-t) rather than t2(t)
+*)
+fun cancel (c $ lhs $ rhs) =
+  let
+    val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false;
+    val (pos, l) = find_common opp (atoms lhs) (atoms rhs);
+    val posr = if opp then not pos else pos;
+  in c $ the (zerofy (pos, l) lhs) $ the (zerofy (posr, l) rhs) end;
+
+
+(** prove cancellation **)
+
+fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
+      [@{const_name Groups.zero}, @{const_name Groups.plus},
+        @{const_name Groups.uminus}, @{const_name Groups.minus}]
+  | agrp_ord _ = ~1;
+
+fun less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
+
+fun solve (_ $ (Const (@{const_name Groups.plus}, _) $ _ $ _) $ _) =
+      SOME @{thm add_assoc [THEN eq_reflection]}
+  | solve (_ $ x $ (Const (@{const_name Groups.plus}, _) $ y $ _)) =
+      if less_agrp (y, x) then
+        SOME @{thm add_left_commute [THEN eq_reflection]}
+        else NONE
+  | solve (_ $ x $ y) =
+      if less_agrp (y, x) then
+        SOME @{thm add_commute [THEN eq_reflection]} else
+        NONE
+  | solve _ = NONE;
+  
+val simproc = Simplifier.simproc @{theory}
+  "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
+
+val cancel_ss = HOL_basic_ss settermless less_agrp
+  addsimprocs [simproc] addsimps
+  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
+   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
+   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
+   @{thm minus_add_cancel}];
+
+fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss);
+
+
+(** simprocs **)
+
+(* cancel complementary terms in arbitrary sums *)
+
+fun sum_proc ss ct =
+  let
+    val t = Thm.term_of ct;
+    val prop = Logic.mk_equals (t, cancel t);
+    val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
+      (fn _ => cancel_simp_tac ss 1)
+  in SOME thm end handle Cancel => NONE;
+
+
+(* cancel like terms on the opposite sides of relations:
+    (x + y - z < -z + x) = (y < 0)
+   Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
+   Reduces the problem to subtraction. *)
+
+fun rel_proc ss ct =
+  let
+    val t = Thm.term_of ct;
+    val prop = Logic.mk_equals (t, cancel t);
+    val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
+      (fn _ => rtac @{thm eq_reflection} 1 THEN
+        resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN
+        cancel_simp_tac ss 1)
+  in SOME thm end handle Cancel => NONE;
+
+end;
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -818,7 +818,7 @@
         @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
         @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
         @{thm "not_one_less_zero"}]
-      addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
+      addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
        (*abel_cancel helps it work in abstract algebraic domains*)
       addsimprocs Nat_Arith.nat_cancel_sums_add
       addcongs [@{thm if_weak_cong}],
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Tools/list_code.ML
--- a/src/HOL/Tools/list_code.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/list_code.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -46,8 +46,8 @@
             Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
         | NONE =>
             default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
-  in Code_Target.add_syntax_const target
-    @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
+  in Code_Target.add_syntax_const target @{const_name Cons}
+    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
   end
 
 end;
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/numeral.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -77,8 +77,8 @@
       (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
     thy |> Code_Target.add_syntax_const target number_of
-      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
-        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
   end;
 
 end; (*local*)
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/string_code.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -60,7 +60,7 @@
         | NONE =>
             List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   in Code_Target.add_syntax_const target
-    @{const_name Cons} (SOME (2, (cs_summa, pretty)))
+    @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
   end;
 
 fun add_literal_char target =
@@ -70,7 +70,7 @@
        of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
         | NONE => Code_Printer.eqn_error thm "Illegal character expression";
   in Code_Target.add_syntax_const target
-    @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
+    @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
   end;
 
 fun add_literal_string target =
@@ -83,7 +83,7 @@
               | NONE => Code_Printer.eqn_error thm "Illegal message expression")
         | NONE => Code_Printer.eqn_error thm "Illegal message expression";
   in Code_Target.add_syntax_const target 
-    @{const_name STR} (SOME (1, (cs_summa, pretty)))
+    @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
   end;
 
 end;
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Transcendental.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Wed Jul 21 16:50:42 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 496d723516e6 -r eb89d0ac75fb src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Word/Word.thy	Wed Jul 21 16:50:42 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 
diff -r 496d723516e6 -r eb89d0ac75fb src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/ex/Lagrange.thy	Wed Jul 21 16:50:42 2010 +0200
@@ -22,12 +22,6 @@
 However, this is an abstract theorem about commutative rings.  It has,
 a priori, nothing to do with nat. *}
 
-(* These two simprocs are even less efficient than ordered rewriting
-   and kill the second example: *)
-ML {*
-  Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
-*}
-
 lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
   "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
diff -r 496d723516e6 -r eb89d0ac75fb src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Wed Jul 21 16:49:52 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(*  Title:      Provers/Arith/abel_cancel.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Simplification procedures for abelian groups (e.g. integers, reals,
-polymorphic types).
-
-- Cancel complementary terms in sums
-- Cancel like terms on opposite sides of relations
-*)
-
-signature ABEL_CANCEL =
-sig
-  val eq_reflection   : thm           (*object-equality to meta-equality*)
-  val T               : typ           (*the type of group elements*)
-  val cancel_ss       : simpset       (*abelian group cancel simpset*)
-  val sum_pats        : cterm list
-  val eqI_rules       : thm list
-  val dest_eqI        : thm -> term
-end;
-
-
-functor Abel_Cancel (Data: ABEL_CANCEL) =
-struct
-
-open Data;
-
-(* FIXME dependent on abstract syntax *)
-
-fun zero t = Const (@{const_name Groups.zero}, t);
-fun minus t = Const (@{const_name Groups.uminus}, t --> t);
-
-fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
-      add_terms pos (x, add_terms pos (y, ts))
-  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
-      add_terms pos (x, add_terms (not pos) (y, ts))
-  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
-      add_terms (not pos) (x, ts)
-  | add_terms pos (x, ts) = (pos,x) :: ts;
-
-fun terms fml = add_terms true (fml, []);
-
-fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
-      (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
-                                   | SOME z => SOME(c $ x $ z))
-       | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
-      (case zero1 (pos,t) x of
-         NONE => (case zero1 (not pos,t) y of NONE => NONE
-                  | SOME z => SOME(c $ x $ z))
-       | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
-      (case zero1 (not pos,t) x of NONE => NONE
-       | SOME z => SOME(c $ z))
-  | zero1 (pos,t) u =
-      if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
-
-exception Cancel;
-
-fun find_common _ [] _ = raise Cancel
-  | find_common opp ((p,l)::ls) rs =
-      let val pr = if opp then not p else p
-      in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
-         else find_common opp ls rs
-      end
-
-(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
-   If OP = +, it must be t2(-t) rather than t2(t)
-*)
-fun cancel t =
-  let
-    val c $ lhs $ rhs = t
-    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
-    val (pos,l) = find_common opp (terms lhs) (terms rhs)
-    val posr = if opp then not pos else pos
-    val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
-  in t' end;
-
-
-(*A simproc to cancel complementary terms in arbitrary sums.*)
-fun sum_proc ss t =
-   let
-     val t' = cancel t
-     val thm =
-       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
-         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
-   in SOME thm end handle Cancel => NONE;
-
-val sum_conv =
-  Simplifier.mk_simproc "cancel_sums"
-    (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
-
-
-(*A simproc to cancel like terms on the opposite sides of relations:
-   (x + y - z < -z + x) = (y < 0)
-  Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
-  Reduces the problem to subtraction.*)
-fun rel_proc ss t =
-  let
-    val t' = cancel t
-    val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
-      (fn _ => rtac eq_reflection 1 THEN
-                    resolve_tac eqI_rules 1 THEN
-                    simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
-   in SOME thm end handle Cancel => NONE;
-
-val rel_conv =
-  Simplifier.mk_simproc "cancel_relations"
-    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
-
-end;
diff -r 496d723516e6 -r eb89d0ac75fb src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -77,6 +77,9 @@
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring -> unit
   val print_registrations: theory -> string -> unit
+  val locale_deps: theory ->
+    { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
+      * term list list Symtab.table Symtab.table
 end;
 
 structure Locale: LOCALE =
@@ -567,10 +570,10 @@
 
 (*** diagnostic commands and interfaces ***)
 
-fun all_locales thy = map #1 (Name_Space.extern_table (Locales.get thy));
+val all_locales = Symtab.keys o snd o Locales.get;
 
 fun print_locales thy =
-  Pretty.strs ("locales:" :: all_locales thy)
+  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   |> Pretty.writeln;
 
 fun print_locale thy show_facts raw_name =
@@ -593,4 +596,32 @@
     | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   |> Pretty.writeln;
 
+fun locale_deps thy =
+  let
+    val names = all_locales thy
+    fun add_locale_node name =
+      let
+        val params = params_of thy name;
+        val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
+        val registrations = map (instance_of thy name o snd)
+          (these_registrations thy name);
+      in 
+        Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
+      end;
+    fun add_locale_deps name =
+      let
+        val dependencies = (map o apsnd) (instance_of thy name o op $>)
+          (dependencies_of thy name);
+      in
+        fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
+          deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
+            dependencies
+      end;
+  in
+    Graph.empty
+    |> fold add_locale_node names
+    |> rpair Symtab.empty
+    |> fold add_locale_deps names
+  end;
+
 end;
diff -r 496d723516e6 -r eb89d0ac75fb src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -218,30 +218,35 @@
       | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
-             of NONE => semicolon [
-                    (str o deresolve_base) classparam,
-                    str "=",
-                    print_app tyvars (SOME thm) reserved NOBR (const, [])
-                  ]
-              | SOME (k, pr) =>
-                  let
-                    val (c, (_, tys)) = const;
-                    val (vs, rhs) = (apfst o map) fst
-                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
-                    val s = if (is_some o syntax_const) c
-                      then NONE else (SOME o Long_Name.base_name o deresolve) c;
-                    val vars = reserved
-                      |> intro_vars (map_filter I (s :: vs));
-                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
-                      (*dictionaries are not relevant at this late stage*)
-                  in
-                    semicolon [
-                      print_term tyvars (SOME thm) vars NOBR lhs,
+            fun requires_args classparam = case syntax_const classparam
+             of NONE => 0
+              | SOME (Code_Printer.Plain_const_syntax _) => 0
+              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
+            fun print_classparam_instance ((classparam, const), (thm, _)) =
+              case requires_args classparam
+               of 0 => semicolon [
+                      (str o deresolve_base) classparam,
                       str "=",
-                      print_term tyvars (SOME thm) vars NOBR rhs
+                      print_app tyvars (SOME thm) reserved NOBR (const, [])
                     ]
-                  end;
+                | k =>
+                    let
+                      val (c, (_, tys)) = const;
+                      val (vs, rhs) = (apfst o map) fst
+                        (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+                      val s = if (is_some o syntax_const) c
+                        then NONE else (SOME o Long_Name.base_name o deresolve) c;
+                      val vars = reserved
+                        |> intro_vars (map_filter I (s :: vs));
+                      val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
+                        (*dictionaries are not relevant at this late stage*)
+                    in
+                      semicolon [
+                        print_term tyvars (SOME thm) vars NOBR lhs,
+                        str "=",
+                        print_term tyvars (SOME thm) vars NOBR rhs
+                      ]
+                    end;
           in
             Pretty.block_enclose (
               Pretty.block [
@@ -459,7 +464,7 @@
   in if target = target' then
     thy
     |> Code_Target.add_syntax_const target c_bind
-        (SOME (pretty_haskell_monad c_bind))
+        (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
   else error "Only Haskell target allows for monad syntax" end;
 
 
diff -r 496d723516e6 -r eb89d0ac75fb src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -67,20 +67,22 @@
 
   type tyco_syntax
   type simple_const_syntax
-  type proto_const_syntax
+  type complex_const_syntax
   type const_syntax
-  val parse_infix: ('a -> 'b) -> lrx * int -> string
-    -> int * ((fixity -> 'b -> Pretty.T)
-    -> fixity -> 'a list -> Pretty.T)
-  val parse_syntax: ('a -> 'b) -> Token.T list
-    -> (int * ((fixity -> 'b -> Pretty.T)
-    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
-  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
+  type activated_complex_const_syntax
+  datatype activated_const_syntax = Plain_const_syntax of int * string
+    | Complex_const_syntax of activated_complex_const_syntax
+  val requires_args: const_syntax -> int
+  val parse_const_syntax: Token.T list -> const_syntax option * Token.T list
+  val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list
+  val plain_const_syntax: string -> const_syntax
+  val simple_const_syntax: simple_const_syntax -> const_syntax
+  val complex_const_syntax: complex_const_syntax -> const_syntax
   val activate_const_syntax: theory -> literals
-    -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
+    -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
   val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-    -> (string -> const_syntax option)
+    -> (string -> activated_const_syntax option)
     -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> fixity
@@ -243,31 +245,45 @@
 
 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   -> fixity -> (iterm * itype) list -> Pretty.T);
-type proto_const_syntax = int * (string list * (literals -> string list
+
+type complex_const_syntax = int * (string list * (literals -> string list
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
-type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+
+datatype const_syntax = plain_const_syntax of string
+  | complex_const_syntax of complex_const_syntax;
+
+fun requires_args (plain_const_syntax _) = 0
+  | requires_args (complex_const_syntax (k, _)) = k;
 
 fun simple_const_syntax syn =
-  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
+  complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
 
-fun activate_const_syntax thy literals (n, (cs, f)) naming =
-  fold_map (Code_Thingol.ensure_declared_const thy) cs naming
-  |-> (fn cs' => pair (n, f literals cs'));
+type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
+
+datatype activated_const_syntax = Plain_const_syntax of int * string
+  | Complex_const_syntax of activated_complex_const_syntax;
 
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
+fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
+      (Plain_const_syntax (Code.args_number thy c, s), naming)
+  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
+      fold_map (Code_Thingol.ensure_declared_const thy) cs naming
+      |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
+
+fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
   case syntax_const c
-   of NONE => brackify fxy (print_app_expr thm vars app)
-    | SOME (k, print) =>
+   of NONE => brackify fxy (print_app_expr some_thm vars app)
+    | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+    | SOME (Complex_const_syntax (k, print)) =>
         let
-          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
+          fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
         in if k = length ts
           then print' fxy ts
         else if k < length ts
           then case chop k ts of (ts1, ts2) =>
-            brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2)
-          else print_term thm vars fxy (Code_Thingol.eta_expand k app)
+            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
 fun gen_print_bind print_term thm (fxy : fixity) pat vars =
@@ -281,7 +297,8 @@
 
 datatype 'a mixfix =
     Arg of fixity
-  | Pretty of Pretty.T;
+  | String of string
+  | Break;
 
 fun mk_mixfix prep_arg (fixity_this, mfx) =
   let
@@ -292,8 +309,10 @@
           []
       | fillin print (Arg fxy :: mfx) (a :: args) =
           (print fxy o prep_arg) a :: fillin print mfx args
-      | fillin print (Pretty p :: mfx) args =
-          p :: fillin print mfx args;
+      | fillin print (String s :: mfx) args =
+          str s :: fillin print mfx args
+      | fillin print (Break :: mfx) args =
+          Pretty.brk 1 :: fillin print mfx args;
   in
     (i, fn print => fn fixity_ctxt => fn args =>
       gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
@@ -304,42 +323,45 @@
     val l = case x of L => INFX (i, L) | _ => INFX (i, X);
     val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   in
-    mk_mixfix prep_arg (INFX (i, x),
-      [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+    mk_mixfix prep_arg (INFX (i, x), [Arg l, String " ", String s, Break, Arg r])
   end;
 
-fun parse_mixfix prep_arg s =
+fun parse_mixfix mk_plain mk_complex prep_arg s =
   let
     val sym_any = Scan.one Symbol.is_regular;
     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))
-      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
+      || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
       || (Scan.repeat1
            (   $$ "'" |-- sym_any
             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
-                 sym_any) >> (Pretty o str o implode)));
+                 sym_any) >> (String o implode)));
   in case Scan.finite Symbol.stopper parse (Symbol.explode s)
-   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
-    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
+   of ((false, [String s]), []) => mk_plain s
+    | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
+    | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
     | _ => Scan.!!
         (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   end;
 
 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
 
-fun parse_syntax prep_arg xs =
-  Scan.option ((
+fun parse_syntax mk_plain mk_complex prep_arg =
+  Scan.option (
       ((Parse.$$$ infixK >> K X)
         || (Parse.$$$ infixlK >> K L)
         || (Parse.$$$ infixrK >> K R))
-        -- Parse.nat >> parse_infix prep_arg
-      || Scan.succeed (parse_mixfix prep_arg))
-      -- Parse.string
-      >> (fn (parse, s) => parse s)) xs;
+        -- Parse.nat -- Parse.string
+        >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
+      || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
 
 val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
 
+val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I;
+
+val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
+
 
 (** module name spaces **)
 
diff -r 496d723516e6 -r eb89d0ac75fb src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -76,17 +76,20 @@
         (app as ((c, ((arg_typs, _), function_typs)), ts)) =
       let
         val k = length ts;
-        val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
         val arg_typs' = if is_pat orelse
           (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
-        val (no_syntax, print') = case syntax_const c
-         of NONE => (true, fn ts => applify "(" ")"
+        val (l, print') = case syntax_const c
+         of NONE => (args_num c, fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR ((str o deresolve) c) arg_typs') ts)
-          | SOME (_, print) => (false, fn ts =>
-              print (print_term tyvars is_pat some_thm) some_thm vars fxy
-                (ts ~~ take l function_typs));
+          | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
+              (print_term tyvars is_pat some_thm vars NOBR) fxy
+                (applify "[" "]" (print_typ tyvars NOBR)
+                  NOBR (str s) arg_typs') ts)
+          | SOME (Complex_const_syntax (k, print)) =>
+              (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
+                (ts ~~ take k function_typs))
       in if k = l then print' ts
       else if k < l then
         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -211,7 +214,7 @@
                   ];
           in
             Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
-              NOBR ((concat o map str) ["sealed", "class", deresolve_base name]) vs
+              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_base name]) vs
                 :: map print_co cos)
           end
       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
@@ -355,20 +358,22 @@
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
       reserved args_num is_singleton_constr deresolver;
-    fun print_module name content =
-      (name, Pretty.chunks [
-        str ("object " ^ name ^ " {"),
-        str "",
+    fun print_module name imports content =
+      (name, Pretty.chunks (
+        str ("object " ^ name ^ " {")
+        :: (if null imports then []
+          else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
+        @ [str "",
         content,
         str "",
-        str "}"
-      ]);
+        str "}"]
+      ));
     fun serialize_module the_module_name sca_program =
       let
         val content = Pretty.chunks2 (map_filter
           (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
             | (_, (_, NONE)) => NONE) sca_program);
-      in print_module the_module_name content end;
+      in print_module the_module_name (map fst includes) content end;
     fun check_destination destination =
       (File.check destination; destination);
     fun write_module destination (modlname, content) =
@@ -385,7 +390,7 @@
       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
         (write_module (check_destination file)))
       (rpair [] o cat_lines o map (code_of_pretty o snd))
-      (map (uncurry print_module) includes
+      (map (fn (name, content) => print_module name [] content) includes
         @| serialize_module the_module_name sca_program)
       destination
   end;
@@ -405,7 +410,7 @@
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
-  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
   literal_naive_numeral = fn k => if k >= 0
     then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
diff -r 496d723516e6 -r eb89d0ac75fb src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Jul 21 16:50:42 2010 +0200
@@ -41,11 +41,11 @@
 
   val allow_abort: string -> theory -> theory
   type tyco_syntax = Code_Printer.tyco_syntax
-  type proto_const_syntax = Code_Printer.proto_const_syntax
+  type const_syntax = Code_Printer.const_syntax
   val add_syntax_class: string -> class -> string option -> theory -> theory
   val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
   val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
-  val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
+  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
   val add_include: string -> string * (string * string list) option -> theory -> theory
 end;
@@ -57,7 +57,7 @@
 
 type literals = Code_Printer.literals;
 type tyco_syntax = Code_Printer.tyco_syntax;
-type proto_const_syntax = Code_Printer.proto_const_syntax;
+type const_syntax = Code_Printer.const_syntax;
 
 
 (** basics **)
@@ -83,7 +83,7 @@
   class: string Symtab.table,
   instance: unit Symreltab.table,
   tyco: Code_Printer.tyco_syntax Symtab.table,
-  const: Code_Printer.proto_const_syntax Symtab.table
+  const: Code_Printer.const_syntax Symtab.table
 };
 
 fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -108,7 +108,7 @@
   -> (string -> string option)          (*module aliasses*)
   -> (string -> string option)          (*class syntax*)
   -> (string -> Code_Printer.tyco_syntax option)
-  -> (string -> Code_Printer.const_syntax option)
+  -> (string -> Code_Printer.activated_const_syntax option)
   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   -> Code_Thingol.program
   -> string list                        (*selected statements*)
@@ -244,11 +244,11 @@
   |>> map_filter I;
 
 fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
-  |> fold_map (fn thing_identifier => fn (tab, naming) =>
-      case Code_Thingol.lookup_const naming thing_identifier
+  |> fold_map (fn c => fn (tab, naming) =>
+      case Code_Thingol.lookup_const naming c
        of SOME name => let
               val (syn, naming') = Code_Printer.activate_const_syntax thy
-                literals (the (Symtab.lookup src_tab thing_identifier)) naming
+                literals c (the (Symtab.lookup src_tab c)) naming
             in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
         | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
   |>> map_filter I;
@@ -445,12 +445,12 @@
       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
       else syn);
 
-fun gen_add_syntax_const prep_const prep_syn =
+fun gen_add_syntax_const prep_const =
   gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
-    (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
-      if fst syn > Code.args_number thy c
+    (fn thy => fn c => fn syn =>
+      if Code_Printer.requires_args syn > Code.args_number thy c
       then error ("Too many arguments in syntax for constant " ^ quote c)
-      else syn end);
+      else syn);
 
 fun add_reserved target =
   let
@@ -496,22 +496,23 @@
 
 fun zip_list (x::xs) f g =
   f
-  #-> (fn y =>
+  :|-- (fn y =>
     fold_map (fn x => g |-- f >> pair x) xs
-    #-> (fn xys => pair ((x, y) :: xys)));
+    :|-- (fn xys => pair ((x, y) :: xys)));
 
-fun parse_multi_syntax parse_thing parse_syntax =
-  Parse.and_list1 parse_thing
-  #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
-        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
+fun process_multi_syntax parse_thing parse_syntax change =
+  (Parse.and_list1 parse_thing
+  :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
+  >> (Toplevel.theory oo fold)
+    (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
 
 in
 
 val add_syntax_class = gen_add_syntax_class cert_class;
 val add_syntax_inst = gen_add_syntax_inst cert_inst;
 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
-val add_syntax_const = gen_add_syntax_const (K I) I;
+val add_syntax_const = gen_add_syntax_const (K I);
 val allow_abort = gen_allow_abort (K I);
 val add_reserved = add_reserved;
 val add_include = add_include;
@@ -519,9 +520,7 @@
 val add_syntax_class_cmd = gen_add_syntax_class read_class;
 val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
-
+val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
 val allow_abort_cmd = gen_allow_abort Code.read_const;
 
 fun parse_args f args =
@@ -550,32 +549,24 @@
 
 val _ =
   Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
-    parse_multi_syntax Parse.xname (Scan.option Parse.string)
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
-  );
+    process_multi_syntax Parse.xname (Scan.option Parse.string)
+    add_syntax_class_cmd);
 
 val _ =
   Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
-    parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+    process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
       (Scan.option (Parse.minus >> K ()))
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
-  );
+    add_syntax_inst_cmd);
 
 val _ =
   Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
-    parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
-  );
+    process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
+    add_syntax_tyco_cmd);
 
 val _ =
   Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
-    parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
-  );
+    process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+    add_syntax_const_cmd);
 
 val _ =
   Outer_Syntax.command "code_reserved" "declare words as reserved for target language"