# HG changeset patch
# User wenzelm
# Date 1451262508 -3600
# Node ID 1135b8de26c3b3e050428aec1266371a1f27e7f4
# Parent  5d06ecfdb472e6a613cf0d66b4bcabd33c1cdb9e
more symbols;

diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -13,7 +13,7 @@
 
 lemma dvds_eq_abseq:
   fixes k :: int
-  shows "l dvd k \<and> k dvd l \<longleftrightarrow> abs l = abs k"
+  shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
 apply rule
  apply (simp add: zdvd_antisym_abs)
 apply (simp add: dvd_if_abs_eq)
@@ -281,7 +281,7 @@
   finally show ?thesis .
 qed
 
-lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> abs l = abs k"
+lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
   apply (subst dvds_eq_abseq[symmetric])
   apply (rule dvds_eq_Idl[symmetric])
   done
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -170,10 +170,10 @@
 "float_power_bnds prec n l u =
   (if 0 < l then (power_down_fl prec l n, power_up_fl prec u n)
   else if odd n then
-    (- power_up_fl prec (abs l) n,
-      if u < 0 then - power_down_fl prec (abs u) n else power_up_fl prec u n)
-  else if u < 0 then (power_down_fl prec (abs u) n, power_up_fl prec (abs l) n)
-  else (0, power_up_fl prec (max (abs l) (abs u)) n))"
+    (- power_up_fl prec \<bar>l\<bar> n,
+      if u < 0 then - power_down_fl prec \<bar>u\<bar> n else power_up_fl prec u n)
+  else if u < 0 then (power_down_fl prec \<bar>u\<bar> n, power_up_fl prec \<bar>l\<bar> n)
+  else (0, power_up_fl prec (max \<bar>l\<bar> \<bar>u\<bar>) n))"
 
 lemma le_minus_power_downI: "0 \<le> x \<Longrightarrow> x ^ n \<le> - a \<Longrightarrow> a \<le> - power_down prec x n"
   by (subst le_minus_iff) (auto intro: power_down_le power_mono_odd)
@@ -2679,7 +2679,7 @@
 "interpret_floatarith (Arctan a) vs   = arctan (interpret_floatarith a vs)" |
 "interpret_floatarith (Min a b) vs    = min (interpret_floatarith a vs) (interpret_floatarith b vs)" |
 "interpret_floatarith (Max a b) vs    = max (interpret_floatarith a vs) (interpret_floatarith b vs)" |
-"interpret_floatarith (Abs a) vs      = abs (interpret_floatarith a vs)" |
+"interpret_floatarith (Abs a) vs      = \<bar>interpret_floatarith a vs\<bar>" |
 "interpret_floatarith Pi vs           = pi" |
 "interpret_floatarith (Sqrt a) vs     = sqrt (interpret_floatarith a vs)" |
 "interpret_floatarith (Exp a) vs      = exp (interpret_floatarith a vs)" |
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -618,11 +618,11 @@
 | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<noteq> 0 then T else F | _ \<Rightarrow> NEq a')"
 | "simpfm (Dvd i a) =
     (if i = 0 then simpfm (Eq a)
-     else if abs i = 1 then T
+     else if \<bar>i\<bar> = 1 then T
      else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')"
 | "simpfm (NDvd i a) =
     (if i = 0 then simpfm (NEq a)
-     else if abs i = 1 then F
+     else if \<bar>i\<bar> = 1 then F
      else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> NDvd i a')"
 | "simpfm p = p"
   by pat_completeness auto
@@ -718,7 +718,7 @@
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
     by simp
-  consider "i = 0" | "abs i = 1" | "i \<noteq> 0" "abs i \<noteq> 1" by blast
+  consider "i = 0" | "\<bar>i\<bar> = 1" | "i \<noteq> 0" "\<bar>i\<bar> \<noteq> 1" by blast
   then show ?case
   proof cases
     case 1
@@ -740,7 +740,7 @@
     proof cases
       case 1
       with sa[symmetric] i show ?thesis
-        by (cases "abs i = 1") auto
+        by (cases "\<bar>i\<bar> = 1") auto
     next
       case 2
       then have "simpfm (Dvd i a) = Dvd i ?sa"
@@ -753,7 +753,7 @@
   let ?sa = "simpnum a"
   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
     by simp
-  consider "i = 0" | "abs i = 1" | "i \<noteq> 0" "abs i \<noteq> 1" by blast
+  consider "i = 0" | "\<bar>i\<bar> = 1" | "i \<noteq> 0" "\<bar>i\<bar> \<noteq> 1" by blast
   then show ?case
   proof cases
     case 1
@@ -775,7 +775,7 @@
     proof cases
       case 1
       with sa[symmetric] i show ?thesis
-        by (cases "abs i = 1") auto
+        by (cases "\<bar>i\<bar> = 1") auto
     next
       case 2
       then have "simpfm (NDvd i a) = NDvd i ?sa"
@@ -1046,16 +1046,16 @@
     (if i = 0 then zlfm (Eq a)
      else
       let (c, r) = zsplit0 a in
-        if c = 0 then Dvd (abs i) r
-        else if c > 0 then Dvd (abs i) (CN 0 c r)
-        else Dvd (abs i) (CN 0 (- c) (Neg r)))"
+        if c = 0 then Dvd \<bar>i\<bar> r
+        else if c > 0 then Dvd \<bar>i\<bar> (CN 0 c r)
+        else Dvd \<bar>i\<bar> (CN 0 (- c) (Neg r)))"
   "zlfm (NDvd i a) =
     (if i = 0 then zlfm (NEq a)
      else
       let (c, r) = zsplit0 a in
-        if c = 0 then NDvd (abs i) r
-        else if c > 0 then NDvd (abs i) (CN 0 c r)
-        else NDvd (abs i) (CN 0 (- c) (Neg r)))"
+        if c = 0 then NDvd \<bar>i\<bar> r
+        else if c > 0 then NDvd \<bar>i\<bar> (CN 0 c r)
+        else NDvd \<bar>i\<bar> (CN 0 (- c) (Neg r)))"
   "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
   "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
   "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
@@ -1213,7 +1213,7 @@
     case 4
     then have l: "?L (?l (Dvd j a))"
       by (simp add: nb Let_def split_def)
-    with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis
+    with Ia 4 dvd_minus_iff[of "\<bar>j\<bar>" "?c*i + ?N ?r"] show ?thesis
       by (simp add: Let_def split_def)
   qed
 next
@@ -1253,7 +1253,7 @@
     case 4
     then have l: "?L (?l (Dvd j a))"
       by (simp add: nb Let_def split_def)
-    with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis
+    with Ia 4 dvd_minus_iff[of "\<bar>j\<bar>" "?c*i + ?N ?r"] show ?thesis
       by (simp add: Let_def split_def)
   qed
 qed auto
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -455,8 +455,8 @@
 
 fun maxcoeff:: "num \<Rightarrow> int"
 where
-  "maxcoeff (C i) = abs i"
-| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
+  "maxcoeff (C i) = \<bar>i\<bar>"
+| "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
 | "maxcoeff t = 1"
 
 lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
@@ -498,7 +498,7 @@
 
 declare dvd_trans [trans add]
 
-lemma natabs0: "nat (abs x) = 0 \<longleftrightarrow> x = 0"
+lemma natabs0: "nat \<bar>x\<bar> = 0 \<longleftrightarrow> x = 0"
   by arith
 
 lemma numgcd0:
@@ -536,8 +536,8 @@
 
 fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
 where
-  "ismaxcoeff (C i) = (\<lambda>x. abs i \<le> x)"
-| "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> ismaxcoeff t x)"
+  "ismaxcoeff (C i) = (\<lambda>x. \<bar>i\<bar> \<le> x)"
+| "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> ismaxcoeff t x)"
 | "ismaxcoeff t = (\<lambda>x. True)"
 
 lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
@@ -547,18 +547,18 @@
 proof (induct t rule: maxcoeff.induct)
   case (2 n c t)
   then have H:"ismaxcoeff t (maxcoeff t)" .
-  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)"
+  have thh: "maxcoeff t \<le> max \<bar>c\<bar> (maxcoeff t)"
     by simp
   from ismaxcoeff_mono[OF H thh] show ?case
     by simp
 qed simp_all
 
 lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow>
-  abs i > 1 \<and> abs j > 1 \<or> abs i = 0 \<and> abs j > 1 \<or> abs i > 1 \<and> abs j = 0"
-  apply (cases "abs i = 0", simp_all add: gcd_int_def)
-  apply (cases "abs j = 0", simp_all)
-  apply (cases "abs i = 1", simp_all)
-  apply (cases "abs j = 1", simp_all)
+  \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
+  apply (cases "\<bar>i\<bar> = 0", simp_all add: gcd_int_def)
+  apply (cases "\<bar>j\<bar> = 0", simp_all)
+  apply (cases "\<bar>i\<bar> = 1", simp_all)
+  apply (cases "\<bar>j\<bar> = 1", simp_all)
   apply auto
   done
 
@@ -577,7 +577,7 @@
   from 2 have th: "gcd c ?g > 1"
     by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
-  consider "abs c > 1" "?g > 1" | "abs c = 0" "?g > 1" | "?g = 0"
+  consider "\<bar>c\<bar> > 1" "?g > 1" | "\<bar>c\<bar> = 0" "?g > 1" | "?g = 0"
     by auto
   then show ?case
   proof cases
@@ -744,11 +744,11 @@
 lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
 proof (induct t rule: maxcoeff.induct)
   case (2 n c t)
-  then have cnz: "c \<noteq> 0" and mx: "max (abs c) (maxcoeff t) = 0"
+  then have cnz: "c \<noteq> 0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0"
     by simp_all
-  have "max (abs c) (maxcoeff t) \<ge> abs c"
+  have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>"
     by simp
-  with cnz have "max (abs c) (maxcoeff t) > 0"
+  with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0"
     by arith
   with 2 show ?case
     by simp
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -48,19 +48,19 @@
   by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only: of_int_mult[symmetric])
 
 
-lemma rdvd_abs1: "(abs (real_of_int d) rdvd t) = (real_of_int (d ::int) rdvd t)"
+lemma rdvd_abs1: "(\<bar>real_of_int d\<bar> rdvd t) = (real_of_int (d ::int) rdvd t)"
 proof
   assume d: "real_of_int d rdvd t"
   from d int_rdvd_real have d2: "d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
     by auto
 
-  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd \<lfloor>t\<rfloor>" by blast
-  with ti int_rdvd_real[symmetric] have "real_of_int (abs d) rdvd t" by blast
-  thus "abs (real_of_int d) rdvd t" by simp
+  from iffD2[OF abs_dvd_iff] d2 have "\<bar>d\<bar> dvd \<lfloor>t\<rfloor>" by blast
+  with ti int_rdvd_real[symmetric] have "real_of_int \<bar>d\<bar> rdvd t" by blast
+  thus "\<bar>real_of_int d\<bar> rdvd t" by simp
 next
-  assume "abs (real_of_int d) rdvd t" hence "real_of_int (abs d) rdvd t" by simp
-  with int_rdvd_real[where i="abs d" and x="t"]
-  have d2: "abs d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
+  assume "\<bar>real_of_int d\<bar> rdvd t" hence "real_of_int \<bar>d\<bar> rdvd t" by simp
+  with int_rdvd_real[where i="\<bar>d\<bar>" and x="t"]
+  have d2: "\<bar>d\<bar> dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
     by auto
   from iffD1[OF abs_dvd_iff] d2 have "d dvd \<lfloor>t\<rfloor>" by blast
   with ti int_rdvd_real[symmetric] show "real_of_int d rdvd t" by blast
@@ -528,9 +528,9 @@
   "lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
 
 fun maxcoeff:: "num \<Rightarrow> int" where
-  "maxcoeff (C i) = abs i"
-| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
-| "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)"
+  "maxcoeff (C i) = \<bar>i\<bar>"
+| "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
+| "maxcoeff (CF c t s) = max \<bar>c\<bar> (maxcoeff s)"
 | "maxcoeff t = 1"
 
 lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
@@ -602,9 +602,9 @@
 qed (auto simp add: numgcd_def gp)
 
 fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
-  "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
-| "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
-| "ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
+  "ismaxcoeff (C i) = (\<lambda> x. \<bar>i\<bar> \<le> x)"
+| "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
+| "ismaxcoeff (CF c s t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
 | "ismaxcoeff t = (\<lambda>x. True)"
 
 lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
@@ -614,7 +614,7 @@
 proof (induct t rule: maxcoeff.induct)
   case (2 n c t)
   hence H:"ismaxcoeff t (maxcoeff t)" .
-  have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp
+  have thh: "maxcoeff t \<le> max \<bar>c\<bar> (maxcoeff t)" by simp
   from ismaxcoeff_mono[OF H thh] show ?case by simp
 next
   case (3 c t s)
@@ -623,12 +623,12 @@
   from ismaxcoeff_mono[OF H1 thh1] show ?case by simp
 qed simp_all
 
-lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
+lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0))"
   apply (unfold gcd_int_def)
   apply (cases "i = 0", simp_all)
   apply (cases "j = 0", simp_all)
-  apply (cases "abs i = 1", simp_all)
-  apply (cases "abs j = 1", simp_all)
+  apply (cases "\<bar>i\<bar> = 1", simp_all)
+  apply (cases "\<bar>j\<bar> = 1", simp_all)
   apply auto
   done
 
@@ -644,17 +644,17 @@
   let ?g = "numgcdh t m"
   from 2 have th:"gcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
-  have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
-  moreover {assume "abs c > 1" and gp: "?g > 1" with 2
+  have "(\<bar>c\<bar> > 1 \<and> ?g > 1) \<or> (\<bar>c\<bar> = 0 \<and> ?g > 1) \<or> (\<bar>c\<bar> > 1 \<and> ?g = 0)" by simp
+  moreover {assume "\<bar>c\<bar> > 1" and gp: "?g > 1" with 2
     have th: "dvdnumcoeff t ?g" by simp
     have th': "gcd c ?g dvd ?g" by simp
     from dvdnumcoeff_trans[OF th' th] have ?case by simp }
-  moreover {assume "abs c = 0 \<and> ?g > 1"
+  moreover {assume "\<bar>c\<bar> = 0 \<and> ?g > 1"
     with 2 have th: "dvdnumcoeff t ?g" by simp
     have th': "gcd c ?g dvd ?g" by simp
     from dvdnumcoeff_trans[OF th' th] have ?case by simp
     hence ?case by simp }
-  moreover {assume "abs c > 1" and g0:"?g = 0"
+  moreover {assume "\<bar>c\<bar> > 1" and g0:"?g = 0"
     from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
   ultimately show ?case by blast
 next
@@ -662,17 +662,17 @@
   let ?g = "numgcdh t m"
   from 3 have th:"gcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
-  have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
-  moreover {assume "abs c > 1" and gp: "?g > 1" with 3
+  have "(\<bar>c\<bar> > 1 \<and> ?g > 1) \<or> (\<bar>c\<bar> = 0 \<and> ?g > 1) \<or> (\<bar>c\<bar> > 1 \<and> ?g = 0)" by simp
+  moreover {assume "\<bar>c\<bar> > 1" and gp: "?g > 1" with 3
     have th: "dvdnumcoeff t ?g" by simp
     have th': "gcd c ?g dvd ?g" by simp
     from dvdnumcoeff_trans[OF th' th] have ?case by simp }
-  moreover {assume "abs c = 0 \<and> ?g > 1"
+  moreover {assume "\<bar>c\<bar> = 0 \<and> ?g > 1"
     with 3 have th: "dvdnumcoeff t ?g" by simp
     have th': "gcd c ?g dvd ?g" by simp
     from dvdnumcoeff_trans[OF th' th] have ?case by simp
     hence ?case by simp }
-  moreover {assume "abs c > 1" and g0:"?g = 0"
+  moreover {assume "\<bar>c\<bar> > 1" and g0:"?g = 0"
     from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp }
   ultimately show ?case by blast
 qed auto
@@ -904,15 +904,15 @@
 lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
 proof (induct t rule: maxcoeff.induct)
   case (2 n c t)
-  hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
-  have "max (abs c) (maxcoeff t) \<ge> abs c" by simp
-  with cnz have "max (abs c) (maxcoeff t) > 0" by arith
+  hence cnz: "c \<noteq>0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0" by simp+
+  have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>" by simp
+  with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0" by arith
   with 2 show ?case by simp
 next
   case (3 c s t)
-  hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
-  have "max (abs c) (maxcoeff t) \<ge> abs c" by simp
-  with cnz have "max (abs c) (maxcoeff t) > 0" by arith
+  hence cnz: "c \<noteq>0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0" by simp+
+  have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>" by simp
+  with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0" by arith
   with 3 show ?case by simp
 qed auto
 
@@ -1152,10 +1152,10 @@
 | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq (reducecoeff a'))"
 | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq (reducecoeff a'))"
 | "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
-             else if (abs i = 1) \<and> check_int a then T
+             else if (\<bar>i\<bar> = 1) \<and> check_int a then T
              else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in Dvd d t))"
 | "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a)
-             else if (abs i = 1) \<and> check_int a then F
+             else if (\<bar>i\<bar> = 1) \<and> check_int a then F
              else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in NDvd d t))"
 | "simpfm p = p"
 by pat_completeness auto
@@ -1266,10 +1266,10 @@
   ultimately show ?case by blast
 next
   case (12 i a)  let ?sa = "simpnum a"   have sa: "Inum bs ?sa = Inum bs a" by simp
-  have "i=0 \<or> (abs i = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((abs i \<noteq> 1) \<or> (\<not> check_int a)))" by auto
+  have "i=0 \<or> (\<bar>i\<bar> = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)))" by auto
   {assume "i=0" hence ?case using "12.hyps" by (simp add: rdvd_left_0_eq Let_def)}
   moreover
-  {assume ai1: "abs i = 1" and ai: "check_int a"
+  {assume ai1: "\<bar>i\<bar> = 1" and ai: "check_int a"
     hence "i=1 \<or> i= - 1" by arith
     moreover {assume i1: "i = 1"
       from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]]
@@ -1280,9 +1280,9 @@
       have ?case using i1 ai by simp }
     ultimately have ?case by blast}
   moreover
-  {assume inz: "i\<noteq>0" and cond: "(abs i \<noteq> 1) \<or> (\<not> check_int a)"
+  {assume inz: "i\<noteq>0" and cond: "(\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)"
     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
-        by (cases "abs i = 1", auto simp add: int_rdvd_iff) }
+        by (cases "\<bar>i\<bar> = 1", auto simp add: int_rdvd_iff) }
     moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"
       hence th: "simpfm (Dvd i a) = Dvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond by (cases ?sa, auto simp add: Let_def split_def)
       from simpnum_nz have nz:"nozerocoeff ?sa" by simp
@@ -1291,10 +1291,10 @@
   ultimately show ?case by blast
 next
   case (13 i a)  let ?sa = "simpnum a"   have sa: "Inum bs ?sa = Inum bs a" by simp
-  have "i=0 \<or> (abs i = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((abs i \<noteq> 1) \<or> (\<not> check_int a)))" by auto
+  have "i=0 \<or> (\<bar>i\<bar> = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)))" by auto
   {assume "i=0" hence ?case using "13.hyps" by (simp add: rdvd_left_0_eq Let_def)}
   moreover
-  {assume ai1: "abs i = 1" and ai: "check_int a"
+  {assume ai1: "\<bar>i\<bar> = 1" and ai: "check_int a"
     hence "i=1 \<or> i= - 1" by arith
     moreover {assume i1: "i = 1"
       from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]]
@@ -1305,9 +1305,9 @@
       have ?case using i1 ai by simp }
     ultimately have ?case by blast}
   moreover
-  {assume inz: "i\<noteq>0" and cond: "(abs i \<noteq> 1) \<or> (\<not> check_int a)"
+  {assume inz: "i\<noteq>0" and cond: "(\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)"
     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
-        by (cases "abs i = 1", auto simp add: int_rdvd_iff) }
+        by (cases "\<bar>i\<bar> = 1", auto simp add: int_rdvd_iff) }
     moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"
       hence th: "simpfm (NDvd i a) = NDvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond
         by (cases ?sa, auto simp add: Let_def split_def)
@@ -1599,14 +1599,14 @@
       else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))"
   "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
   else (let (c,r) = zsplit0 a in
-              if c=0 then Dvd (abs i) r else
-      if c>0 then And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 c (Floor r)))
-      else And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"
+              if c=0 then Dvd \<bar>i\<bar> r else
+      if c>0 then And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 c (Floor r)))
+      else And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
   "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
   else (let (c,r) = zsplit0 a in
-              if c=0 then NDvd (abs i) r else
-      if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 c (Floor r)))
-      else Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"
+              if c=0 then NDvd \<bar>i\<bar> r else
+      if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 c (Floor r)))
+      else Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
   "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
   "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
   "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
@@ -1865,11 +1865,11 @@
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Dvd j a) = (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r)))"
       using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
+    also have "\<dots> = (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+    also have "\<dots> = (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
        (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
-      by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+      by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
         del: of_int_mult) (auto simp add: ac_simps)
@@ -1879,13 +1879,13 @@
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Dvd j a) = (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r)))"
       using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
+    also have "\<dots> = (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+    also have "\<dots> = (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
        (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
-      by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+      by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
-      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
+      using rdvd_minus [where d="\<bar>j\<bar>" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
         del: of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz by blast }
@@ -1911,11 +1911,11 @@
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (NDvd j a) = (\<not> (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r))))"
       using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
+    also have "\<dots> = (\<not> (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r)))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+    also have "\<dots> = (\<not> (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
        (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
-      by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+      by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
         del: of_int_mult) (auto simp add: ac_simps)
@@ -1925,13 +1925,13 @@
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (NDvd j a) = (\<not> (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r))))"
       using Ia by (simp add: Let_def split_def)
-    also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
+    also have "\<dots> = (\<not> (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r)))"
       by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
-    also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+    also have "\<dots> = (\<not> (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
        (real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
-      by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+      by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
-      using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
+      using rdvd_minus [where d="\<bar>j\<bar>" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]
         del: of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz by blast }
@@ -3261,7 +3261,7 @@
     from iszlfm_gen [OF lp,rule_format, where y="a"] have lp':"iszlfm p (a#bs)" .
     from \<rho>'[OF lp' d dp, rule_format, OF nob] have th:"\<forall> x. ?P x \<longrightarrow> ?P (x - ?d)" by blast
     from minusinf_inf[OF lp] obtain z where z:"\<forall> x<z. ?MP x = ?P x" by blast
-    have zp: "abs (x - z) + 1 \<ge> 0" by arith
+    have zp: "\<bar>x - z\<bar> + 1 \<ge> 0" by arith
     from decr_lemma[OF dp,where x="x" and z="z"]
       decr_mult_lemma[OF dp th zp, rule_format, OF px] z have th:"\<exists> x. ?MP x" by auto
     with minusinf_bex[OF lp] px nob have ?thesis by blast}
@@ -3860,12 +3860,12 @@
 definition DVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
   DVD_def: "DVD i c t =
   (if i=0 then eq c t else
-  if c = 0 then (Dvd i t) else if c >0 then DVDJ (abs i) c t else DVDJ (abs i) (-c) (Neg t))"
+  if c = 0 then (Dvd i t) else if c >0 then DVDJ \<bar>i\<bar> c t else DVDJ \<bar>i\<bar> (-c) (Neg t))"
 
 definition  NDVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
   "NDVD i c t =
   (if i=0 then neq c t else
-  if c = 0 then (NDvd i t) else if c >0 then NDVDJ (abs i) c t else NDVDJ (abs i) (-c) (Neg t))"
+  if c = 0 then (NDvd i t) else if c >0 then NDVDJ \<bar>i\<bar> c t else NDVDJ \<bar>i\<bar> (-c) (Neg t))"
 
 lemma DVD_mono:
   assumes xp: "0\<le> x" and x1: "x < 1"
@@ -5671,7 +5671,7 @@
 lemma "\<forall>x::real. \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
   by mir
 
-lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> \<bar>y - x\<bar> \<and> \<bar>y - x\<bar> \<le> 1"
   by mir
 
 end
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -1118,7 +1118,7 @@
 text \<open>Bound for polynomial.\<close>
 lemma poly_mono:
   fixes x :: "'a::linordered_idom"
-  shows "abs x \<le> k \<Longrightarrow> abs (poly p x) \<le> poly (map abs p) k"
+  shows "\<bar>x\<bar> \<le> k \<Longrightarrow> \<bar>poly p x\<bar> \<le> poly (map abs p) k"
 proof (induct p)
   case Nil
   then show ?case by simp
@@ -1126,7 +1126,7 @@
   case (Cons a p)
   then show ?case
     apply auto
-    apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
+    apply (rule_tac y = "\<bar>a\<bar> + \<bar>x * poly p x\<bar>" in order_trans)
     apply (rule abs_triangle_ineq)
     apply (auto intro!: mult_mono simp add: abs_mult)
     done
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/BigO.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -35,19 +35,19 @@
 subsection \<open>Definitions\<close>
 
 definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
-  where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
+  where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>}"
 
 lemma bigo_pos_const:
-  "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>
-    (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"
+  "(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
+    (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
   apply auto
   apply (case_tac "c = 0")
   apply simp
   apply (rule_tac x = "1" in exI)
   apply simp
-  apply (rule_tac x = "abs c" in exI)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI)
   apply auto
-  apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")
+  apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
   apply (erule_tac x = x in allE)
   apply force
   apply (rule mult_right_mono)
@@ -55,7 +55,7 @@
   apply (rule abs_ge_zero)
   done
 
-lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
   by (auto simp add: bigo_def bigo_pos_const)
 
 lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
@@ -65,7 +65,7 @@
   apply simp
   apply (rule allI)
   apply (drule_tac x = "xa" in spec)+
-  apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
+  apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
   apply (erule order_trans)
   apply (simp add: ac_simps)
   apply (rule mult_left_mono, assumption)
@@ -110,29 +110,29 @@
   apply (rule subsetI)
   apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
   apply (subst bigo_pos_const [symmetric])+
-  apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI)
+  apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> \<le> \<bar>f n\<bar> then x n else 0" in exI)
   apply (rule conjI)
   apply (rule_tac x = "c + c" in exI)
   apply (clarsimp)
-  apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
+  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
   apply (erule_tac x = xa in allE)
   apply (erule order_trans)
   apply (simp)
-  apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
+  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
   apply (erule order_trans)
   apply (simp add: ring_distribs)
   apply (rule mult_left_mono)
   apply (simp add: abs_triangle_ineq)
   apply (simp add: order_less_le)
-  apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
+  apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
   apply (rule conjI)
   apply (rule_tac x = "c + c" in exI)
   apply auto
-  apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)")
+  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
   apply (erule_tac x = xa in allE)
   apply (erule order_trans)
   apply simp
-  apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
+  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
   apply (erule order_trans)
   apply (simp add: ring_distribs)
   apply (rule mult_left_mono)
@@ -162,8 +162,8 @@
   apply (drule_tac x = "xa" in spec)+
   apply (subgoal_tac "0 \<le> f xa + g xa")
   apply (simp add: ring_distribs)
-  apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")
-  apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa")
+  apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
+  apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
   apply force
   apply (rule add_mono)
   apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
@@ -183,7 +183,7 @@
 
 lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
   apply (auto simp add: bigo_def)
-  apply (rule_tac x = "abs c" in exI)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI)
   apply auto
   apply (drule_tac x = x in spec)+
   apply (simp add: abs_mult [symmetric])
@@ -202,21 +202,21 @@
   apply force
   done
 
-lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
+lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
   apply (unfold bigo_def)
   apply auto
   apply (rule_tac x = 1 in exI)
   apply auto
   done
 
-lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"
+lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
   apply (unfold bigo_def)
   apply auto
   apply (rule_tac x = 1 in exI)
   apply auto
   done
 
-lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"
+lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
   apply (rule equalityI)
   apply (rule bigo_elt_subset)
   apply (rule bigo_abs2)
@@ -224,15 +224,15 @@
   apply (rule bigo_abs)
   done
 
-lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
+lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
   apply (drule set_plus_imp_minus)
   apply (rule set_minus_imp_plus)
   apply (subst fun_diff_def)
 proof -
   assume a: "f - g \<in> O(h)"
-  have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"
+  have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
     by (rule bigo_abs2)
-  also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"
+  also have "\<dots> \<subseteq> O(\<lambda>x. \<bar>f x - g x\<bar>)"
     apply (rule bigo_elt_subset)
     apply (rule bigo_bounded)
     apply force
@@ -246,10 +246,10 @@
     done
   also from a have "\<dots> \<subseteq> O(h)"
     by (rule bigo_elt_subset)
-  finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".
+  finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) \<in> O(h)".
 qed
 
-lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"
+lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
   by (unfold bigo_def, auto)
 
 lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
@@ -257,16 +257,16 @@
   assume "f \<in> g +o O(h)"
   also have "\<dots> \<subseteq> O(g) + O(h)"
     by (auto del: subsetI)
-  also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
+  also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
     apply (subst bigo_abs3 [symmetric])+
     apply (rule refl)
     done
-  also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"
+  also have "\<dots> = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
     by (rule bigo_plus_eq [symmetric]) auto
   finally have "f \<in> \<dots>" .
   then have "O(f) \<subseteq> \<dots>"
     by (elim bigo_elt_subset)
-  also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
+  also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
     by (rule bigo_plus_eq, auto)
   finally show ?thesis
     by (simp add: bigo_abs3 [symmetric])
@@ -279,7 +279,7 @@
   apply (rule_tac x = "c * ca" in exI)
   apply (rule allI)
   apply (erule_tac x = x in allE)+
-  apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))")
+  apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
   apply (erule ssubst)
   apply (subst abs_mult)
   apply (rule mult_mono)
@@ -293,7 +293,7 @@
   apply (rule_tac x = c in exI)
   apply auto
   apply (drule_tac x = x in spec)
-  apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
+  apply (subgoal_tac "\<bar>f x\<bar> * \<bar>b x\<bar> \<le> \<bar>f x\<bar> * (c * \<bar>g x\<bar>)")
   apply (force simp add: ac_simps)
   apply (rule mult_left_mono, assumption)
   apply (rule abs_ge_zero)
@@ -450,7 +450,7 @@
   fixes c :: "'a::linordered_field"
   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
   apply (simp add: bigo_def)
-  apply (rule_tac x = "abs (inverse c)" in exI)
+  apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
   apply (simp add: abs_mult [symmetric])
   done
 
@@ -473,7 +473,7 @@
 
 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
   apply (simp add: bigo_def)
-  apply (rule_tac x = "abs c" in exI)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI)
   apply (auto simp add: abs_mult [symmetric])
   done
 
@@ -486,7 +486,7 @@
   fixes c :: "'a::linordered_field"
   shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
   apply (simp add: bigo_def)
-  apply (rule_tac x = "abs (inverse c)" in exI)
+  apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
   apply (simp add: abs_mult mult.assoc [symmetric])
   done
 
@@ -516,15 +516,15 @@
   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
   apply (simp add: mult.assoc [symmetric] abs_mult)
-  apply (rule_tac x = "abs (inverse c) * ca" in exI)
+  apply (rule_tac x = "\<bar>inverse c\<bar> * ca" in exI)
   apply auto
   done
 
 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
-  apply (rule_tac x = "ca * abs c" in exI)
+  apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
   apply (rule allI)
-  apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))")
+  apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
   apply (erule ssubst)
   apply (subst abs_mult)
   apply (rule mult_left_mono)
@@ -559,10 +559,10 @@
 subsection \<open>Setsum\<close>
 
 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
-    \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
+    \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
   apply (auto simp add: bigo_def)
-  apply (rule_tac x = "abs c" in exI)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI)
   apply (subst abs_of_nonneg) back back
   apply (rule setsum_nonneg)
   apply force
@@ -583,7 +583,7 @@
   done
 
 lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
-    \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>
+    \<exists>c. \<forall>x y. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
   apply (rule bigo_setsum_main)
   apply force
@@ -593,12 +593,12 @@
   done
 
 lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
-    \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>
+    \<exists>c. \<forall>y. \<bar>f y\<bar> \<le> c * (h y) \<Longrightarrow>
       (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
   by (rule bigo_setsum1) auto
 
 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
-    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
+    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
   apply (rule bigo_setsum1)
   apply (rule allI)+
   apply (rule abs_ge_zero)
@@ -616,7 +616,7 @@
 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
       (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
-        O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
+        O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
   apply (rule set_minus_imp_plus)
   apply (subst fun_diff_def)
   apply (subst setsum_subtractf [symmetric])
@@ -631,7 +631,7 @@
       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
         O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
   apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
-      (\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))")
+      (\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)")
   apply (erule ssubst)
   apply (erule bigo_setsum3)
   apply (rule ext)
@@ -715,7 +715,7 @@
 definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
   where "f <o g = (\<lambda>x. max (f x - g x) 0)"
 
-lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"
+lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
   apply (unfold bigo_def)
   apply clarsimp
   apply (rule_tac x = c in exI)
@@ -724,7 +724,7 @@
   apply (erule spec)+
   done
 
-lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"
+lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> f x \<Longrightarrow> g =o O(h)"
   apply (erule bigo_lesseq1)
   apply (rule allI)
   apply (drule_tac x = x in spec)
@@ -741,7 +741,7 @@
   done
 
 lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
-    \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"
+    \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
   apply (erule bigo_lesseq1)
   apply (rule allI)
   apply (subst abs_of_nonneg)
@@ -819,13 +819,13 @@
   apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
   done
 
-lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"
+lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * \<bar>h x\<bar>"
   apply (simp only: lesso_def bigo_alt_def)
   apply clarsimp
   apply (rule_tac x = c in exI)
   apply (rule allI)
   apply (drule_tac x = x in spec)
-  apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0")
+  apply (subgoal_tac "\<bar>max (f x - g x) 0\<bar> = max (f x - g x) 0")
   apply (clarsimp simp add: algebra_simps)
   apply (rule abs_of_nonneg)
   apply (rule max.cobounded2)
@@ -856,7 +856,7 @@
   apply (rule order_le_less_trans)
   apply assumption
   apply (rule order_less_le_trans)
-  apply (subgoal_tac "c * abs (g n) < c * (r / c)")
+  apply (subgoal_tac "c * \<bar>g n\<bar> < c * (r / c)")
   apply assumption
   apply (erule mult_strict_left_mono)
   apply assumption
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -3484,7 +3484,7 @@
   fixes a :: real
   assumes "a \<le> x"
     and "x \<le> b"
-  shows "abs x \<le> max (abs a) (abs b)"
+  shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
   by (metis abs_less_iff assms leI le_max_iff_disj
     less_eq_real_def less_le_not_le less_minus_iff minus_minus)
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Float.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -110,7 +110,7 @@
 lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
   using plus_float [of x "- y"] by simp
 
-lemma abs_float[simp]: "x \<in> float \<Longrightarrow> abs x \<in> float"
+lemma abs_float[simp]: "x \<in> float \<Longrightarrow> \<bar>x\<bar> \<in> float"
   by (cases x rule: linorder_cases[of 0]) auto
 
 lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
@@ -594,7 +594,7 @@
 qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
   by transfer (auto simp add: is_float_zero_def)
 
-qualified lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
+qualified lemma compute_float_abs[code]: "\<bar>Float m e\<bar> = Float \<bar>m\<bar> e"
   by transfer (simp add: abs_mult)
 
 qualified lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
@@ -1186,7 +1186,7 @@
 begin
 
 qualified lemma compute_float_round_down[code]:
-  "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
+  "float_round_down prec (Float m e) = (let d = bitlen \<bar>m\<bar> - int prec in
     if 0 < d then Float (div_twopow m (nat d)) (e + d)
              else Float m e)"
   using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
@@ -1543,8 +1543,8 @@
 
 lemma sum_neq_zeroI:
   fixes a k :: real
-  shows "abs a \<ge> k \<Longrightarrow> abs b < k \<Longrightarrow> a + b \<noteq> 0"
-    and "abs a > k \<Longrightarrow> abs b \<le> k \<Longrightarrow> a + b \<noteq> 0"
+  shows "\<bar>a\<bar> \<ge> k \<Longrightarrow> \<bar>b\<bar> < k \<Longrightarrow> a + b \<noteq> 0"
+    and "\<bar>a\<bar> > k \<Longrightarrow> \<bar>b\<bar> \<le> k \<Longrightarrow> a + b \<noteq> 0"
   by auto
 
 lemma abs_real_le_2_powr_bitlen[simp]: "\<bar>real_of_int m2\<bar> < 2 powr real_of_int (bitlen \<bar>m2\<bar>)"
@@ -1564,7 +1564,7 @@
   fixes ai p q :: int
     and a b :: real
   assumes "a * 2 powr p = ai"
-    and b_le_1: "abs (b * 2 powr (p + 1)) \<le> 1"
+    and b_le_1: "\<bar>b * 2 powr (p + 1)\<bar> \<le> 1"
     and leqp: "q \<le> p"
   shows "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2 * ai + sgn b) * 2 powr (q - p - 1)\<rfloor>"
 proof -
@@ -1576,7 +1576,7 @@
       by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
   next
     case 2
-    then have "b * 2 powr p < abs (b * 2 powr (p + 1))"
+    then have "b * 2 powr p < \<bar>b * 2 powr (p + 1)\<bar>"
       by simp
     also note b_le_1
     finally have b_less_1: "b * 2 powr real_of_int p < 1" .
@@ -1635,7 +1635,7 @@
 lemma log2_abs_int_add_less_half_sgn_eq:
   fixes ai :: int
     and b :: real
-  assumes "abs b \<le> 1/2"
+  assumes "\<bar>b\<bar> \<le> 1/2"
     and "ai \<noteq> 0"
   shows "\<lfloor>log 2 \<bar>real_of_int ai + b\<bar>\<rfloor> = \<lfloor>log 2 \<bar>ai + sgn b / 2\<bar>\<rfloor>"
 proof (cases "b = 0")
@@ -1664,21 +1664,21 @@
   have "\<bar>ai\<bar> = 2 powr k + r"
     using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
 
-  have pos: "abs b < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
+  have pos: "\<bar>b\<bar> < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
     using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
     by (auto simp add: r_def powr_realpow[symmetric] abs_if sgn_if algebra_simps
       split: split_if_asm)
   have less: "\<bar>sgn ai * b\<bar> < 1"
     and less': "\<bar>sgn (sgn ai * b) / 2\<bar> < 1"
-    using \<open>abs b \<le> _\<close> by (auto simp: abs_if sgn_if split: split_if_asm)
+    using \<open>\<bar>b\<bar> \<le> _\<close> by (auto simp: abs_if sgn_if split: split_if_asm)
 
-  have floor_eq: "\<And>b::real. abs b \<le> 1 / 2 \<Longrightarrow>
+  have floor_eq: "\<And>b::real. \<bar>b\<bar> \<le> 1 / 2 \<Longrightarrow>
       \<lfloor>log 2 (1 + (r + b) / 2 powr k)\<rfloor> = (if r = 0 \<and> b < 0 then -1 else 0)"
     using \<open>k \<ge> 0\<close> r r_le
     by (auto simp: floor_log_eq_powr_iff powr_minus_divide field_simps sgn_if)
 
   from \<open>real_of_int \<bar>ai\<bar> = _\<close> have "\<bar>ai + b\<bar> = 2 powr k + (r + sgn ai * b)"
-    using \<open>abs b <= _\<close> \<open>0 \<le> k\<close> r
+    using \<open>\<bar>b\<bar> <= _\<close> \<open>0 \<le> k\<close> r
     by (auto simp add: sgn_if abs_if)
   also have "\<lfloor>log 2 \<dots>\<rfloor> = \<lfloor>log 2 (2 powr k + r + sgn (sgn ai * b) / 2)\<rfloor>"
   proof -
@@ -1690,14 +1690,14 @@
     also
     let ?if = "if r = 0 \<and> sgn ai * b < 0 then -1 else 0"
     have "\<lfloor>log 2 (1 + (r + sgn ai * b) / 2 powr k)\<rfloor> = ?if"
-      using \<open>abs b <= _\<close>
+      using \<open>\<bar>b\<bar> <= _\<close>
       by (intro floor_eq) (auto simp: abs_mult sgn_if)
     also
     have "\<dots> = \<lfloor>log 2 (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k)\<rfloor>"
       by (subst floor_eq) (auto simp: sgn_if)
     also have "k + \<dots> = \<lfloor>log 2 (2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k))\<rfloor>"
       unfolding floor_add2[symmetric]
-      using pos[OF less'] \<open>abs b \<le> _\<close>
+      using pos[OF less'] \<open>\<bar>b\<bar> \<le> _\<close>
       by (simp add: field_simps add_log_eq_powr)
     also have "2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k) =
         2 powr k + r + sgn (sgn ai * b) / 2"
@@ -1885,7 +1885,7 @@
 lemma float_zero[simp]: "real_of_float (Float 0 e) = 0"
   by simp
 
-lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
+lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> \<bar>(a::int) div 2\<bar> < \<bar>a\<bar>"
   by arith
 
 lemma lapprox_rat: "real_of_float (lapprox_rat prec x y) \<le> real_of_int x / real_of_int y"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -136,9 +136,9 @@
   proof -
     from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
       by (simp_all add: cmod_def power2_eq_square algebra_simps)
-    then have "abs (2 * x) \<le> 1" "abs (2 * y) \<le> 1"
+    then have "\<bar>2 * x\<bar> \<le> 1" "\<bar>2 * y\<bar> \<le> 1"
       by simp_all
-    then have "(abs (2 * x))\<^sup>2 \<le> 1\<^sup>2" "(abs (2 * y))\<^sup>2 \<le> 1\<^sup>2"
+    then have "\<bar>2 * x\<bar>\<^sup>2 \<le> 1\<^sup>2" "\<bar>2 * y\<bar>\<^sup>2 \<le> 1\<^sup>2"
       by - (rule power_mono, simp, simp)+
     then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
       by (simp_all add: power_mult_distrib)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -56,12 +56,12 @@
 lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
   by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
 
-proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n \<ge> m \<and> n \<in> S)"
+proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
   apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
   apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
   done
 
-proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n > m \<and> n \<in> S)"
+proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)"
   apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
   apply (metis (full_types) nat_le_iff nat_mono not_le)
   done
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -1062,7 +1062,7 @@
   "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
 
 definition
-  "abs (x::'a poly) = (if x < 0 then - x else x)"
+  "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)"
 
 definition
   "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Mon Dec 28 01:28:28 2015 +0100
@@ -221,12 +221,12 @@
       @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
 
 val real_abs_thms1 = @{lemma
-  "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
-  "((-1 * abs(x) + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
-  "((a + -1 * abs(x) >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
-  "((a + -1 * abs(x) + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
-  "((a + b + -1 * abs(x) >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
-  "((a + b + -1 * abs(x) + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
+  "((-1 * \<bar>x::real\<bar> >= r) = (-1 * x >= r & 1 * x >= r))" and
+  "((-1 * \<bar>x\<bar> + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
+  "((a + -1 * \<bar>x\<bar> >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
+  "((a + -1 * \<bar>x\<bar> + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
+  "((a + b + -1 * \<bar>x\<bar> >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
+  "((a + b + -1 * \<bar>x\<bar> + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
   "((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and
   "((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
   "((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
@@ -245,12 +245,12 @@
   "((a + min x y + b >= r) = (a + x + b >= r & a + y  + b >= r))" and
   "((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and
   "((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and
-  "((-1 * abs(x) > r) = (-1 * x > r & 1 * x > r))" and
-  "((-1 * abs(x) + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
-  "((a + -1 * abs(x) > r) = (a + -1 * x > r & a + 1 * x > r))" and
-  "((a + -1 * abs(x) + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
-  "((a + b + -1 * abs(x) > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
-  "((a + b + -1 * abs(x) + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
+  "((-1 * \<bar>x\<bar> > r) = (-1 * x > r & 1 * x > r))" and
+  "((-1 * \<bar>x\<bar> + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
+  "((a + -1 * \<bar>x\<bar> > r) = (a + -1 * x > r & a + 1 * x > r))" and
+  "((a + -1 * \<bar>x\<bar> + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
+  "((a + b + -1 * \<bar>x\<bar> > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
+  "((a + b + -1 * \<bar>x\<bar> + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
   "((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and
   "((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and
   "((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and
@@ -265,7 +265,7 @@
   "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
   by auto};
 
-val abs_split' = @{lemma "P (abs (x::'a::linordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
+val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
   by (atomize (full)) (auto split add: abs_split)};
 
 val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -106,7 +106,7 @@
 lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
 by (rule zmod_int)
 
-lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
+lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> \<bar>(a::int) div 2\<bar> < \<bar>a\<bar>"
 by arith
 
 lemma norm_0_1: "(1::_::numeral) = Numeral1"
@@ -195,7 +195,7 @@
   by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
 
 lemma float_abs:
-  "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
+  "\<bar>float (a,b)\<bar> = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
   by (simp add: float_def abs_if mult_less_0_iff not_less)
 
 lemma float_zero:
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Matrix_LP/LP.thy
--- a/src/HOL/Matrix_LP/LP.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/LP.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -19,47 +19,47 @@
   assumes
   "A * x \<le> (b::'a::lattice_ring)"
   "0 \<le> y"
-  "abs (A - A') \<le> \<delta>_A"
+  "\<bar>A - A'\<bar> \<le> \<delta>_A"
   "b \<le> b'"
-  "abs (c - c') \<le> \<delta>_c"
-  "abs x \<le> r"
+  "\<bar>c - c'\<bar> \<le> \<delta>_c"
+  "\<bar>x\<bar> \<le> r"
   shows
-  "c * x \<le> y * b' + (y * \<delta>_A + abs (y * A' - c') + \<delta>_c) * r"
+  "c * x \<le> y * b' + (y * \<delta>_A + \<bar>y * A' - c'\<bar> + \<delta>_c) * r"
 proof -
   from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
   from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps)  
   from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
-  have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
+  have 5: "c * x <= y * b' + \<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"
     by (simp only: 4 estimate_by_abs)  
-  have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
+  have 6: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= \<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar> * \<bar>x\<bar>"
     by (simp add: abs_le_mult)
-  have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
+  have 7: "(\<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>"
     by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
-  have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <=  (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
+  have 8: "(\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>"
     by (simp add: abs_triangle_ineq mult_right_mono)    
-  have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
+  have 9: "(\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar>"
     by (simp add: abs_le_mult mult_right_mono)  
   have 10: "c'-c = -(c-c')" by (simp add: algebra_simps)
-  have 11: "abs (c'-c) = abs (c-c')" 
+  have 11: "\<bar>c'-c\<bar> = \<bar>c-c'\<bar>"
     by (subst 10, subst abs_minus_cancel, simp)
-  have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>_c) * abs x"
+  have 12: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>"
     by (simp add: 11 assms mult_right_mono)
-  have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>_c) * abs x <= (abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * abs x"
+  have 13: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>"
     by (simp add: assms mult_right_mono mult_left_mono)  
-  have r: "(abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * abs x <=  (abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * r"
+  have r: "(\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r"
     apply (rule mult_left_mono)
     apply (simp add: assms)
     apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
     apply (rule mult_left_mono[of "0" "\<delta>_A", simplified])
     apply (simp_all)
-    apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
-    apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
+    apply (rule order_trans[where y="\<bar>A-A'\<bar>"], simp_all add: assms)
+    apply (rule order_trans[where y="\<bar>c-c'\<bar>"], simp_all add: assms)
     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"     
+  from 6 7 8 9 12 13 r have 14: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r"
     by (simp)
   show ?thesis
-    apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+    apply (rule le_add_right_mono[of _ _ "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"])
     apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]])
     done
 qed
@@ -68,14 +68,14 @@
   assumes
   "A1 <= (A::'a::lattice_ring)"
   "A <= A2" 
-  shows "abs (A-A1) <= A2-A1"
+  shows "\<bar>A-A1\<bar> <= A2-A1"
 proof -
   have "0 <= A - A1"    
   proof -
     from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp
   qed
-  then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
-  with assms show "abs (A-A1) <= (A2-A1)" by simp
+  then have "\<bar>A-A1\<bar> = A-A1" by (rule abs_of_nonneg)
+  with assms show "\<bar>A-A1\<bar> <= (A2-A1)" by simp
 qed
 
 lemma mult_le_prts:
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -918,8 +918,8 @@
 apply (simp add: move_matrix_def)
 apply (auto)
 by (subst RepAbs_matrix,
-  rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
-  rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
+  rule exI[of _ "(nrows A)+(nat \<bar>y\<bar>)"], auto, rule nrows, arith,
+  rule exI[of _ "(ncols A)+(nat \<bar>x\<bar>)"], auto, rule ncols, arith)+
 
 lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
 by (simp add: move_matrix_def)
@@ -1496,7 +1496,7 @@
 begin
 
 definition
-  abs_matrix_def: "abs (A :: 'a matrix) = sup A (- A)"
+  abs_matrix_def: "\<bar>A :: 'a matrix\<bar> = sup A (- A)"
 
 instance ..
 
@@ -1613,7 +1613,7 @@
 instance matrix :: (lattice_ring) lattice_ring
 proof
   fix A B C :: "('a :: lattice_ring) matrix"
-  show "abs A = sup A (-A)" 
+  show "\<bar>A\<bar> = sup A (-A)" 
     by (simp add: abs_matrix_def)
 qed
 
@@ -1814,7 +1814,7 @@
 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"
 by (simp add: minus_matrix_def)
 
-lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)"
+lemma Rep_abs[simp]: "Rep_matrix \<bar>A::_::lattice_ab_group_add\<bar> x y = \<bar>Rep_matrix A x y\<bar>"
 by (simp add: abs_lattice sup_matrix_def)
 
 end
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Matrix_LP/SparseMatrix.thy
--- a/src/HOL/Matrix_LP/SparseMatrix.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -108,7 +108,7 @@
 primrec abs_spvec :: "('a::lattice_ab_group_add_abs) spvec \<Rightarrow> 'a spvec"
 where
   "abs_spvec [] = []"
-| "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
+| "abs_spvec (a#as) = (fst a, \<bar>snd a\<bar>)#(abs_spvec as)"
 
 lemma sparse_row_vector_minus: 
   "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
@@ -127,7 +127,7 @@
   (*FIXME move*)
 
 lemma sparse_row_vector_abs:
-  "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
+  "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = \<bar>sparse_row_vector v\<bar>"
   apply (induct v)
   apply simp_all
   apply (frule_tac sorted_spvec_cons1, simp)
@@ -770,7 +770,7 @@
 qed
     
 lemma sparse_row_matrix_abs:
-  "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = abs (sparse_row_matrix A)"
+  "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = \<bar>sparse_row_matrix A\<bar>"
   apply (induct A)
   apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
   apply (frule_tac sorted_spvec_cons1, simp)
@@ -1060,7 +1060,7 @@
   "A <= sparse_row_matrix A2"
   "sparse_row_matrix c1 <= c"
   "c <= sparse_row_matrix c2"
-  "abs x \<le> sparse_row_matrix r"
+  "\<bar>x\<bar> \<le> sparse_row_matrix r"
   shows
   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, mult_spmat (add_spmat (add_spmat (mult_spmat y (diff_spmat A2 A1), 
   abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -17,12 +17,12 @@
 subsection {* Definitions *}
 
 definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
-  "O(f::('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"
+  "O(f::('a => 'b)) == {h. \<exists>c. \<forall>x. \<bar>h x\<bar> <= c * \<bar>f x\<bar>}"
 
 lemma bigo_pos_const:
   "(\<exists>c::'a::linordered_idom.
-    \<forall>x. abs (h x) \<le> c * abs (f x))
-    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+    \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
   by (metis (no_types) abs_ge_zero
       algebra_simps mult.comm_neutral
       mult_nonpos_nonneg not_le_imp_less order_trans zero_less_one)
@@ -33,12 +33,12 @@
 
 lemma
   "(\<exists>c::'a::linordered_idom.
-    \<forall>x. abs (h x) \<le> c * abs (f x))
-    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+    \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -64,12 +64,12 @@
 
 lemma
   "(\<exists>c::'a::linordered_idom.
-    \<forall>x. abs (h x) \<le> c * abs (f x))
-    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+    \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -87,12 +87,12 @@
 
 lemma
   "(\<exists>c::'a::linordered_idom.
-    \<forall>x. abs (h x) \<le> c * abs (f x))
-    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+    \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -107,12 +107,12 @@
 
 lemma
   "(\<exists>c::'a::linordered_idom.
-    \<forall>x. abs (h x) \<le> c * abs (f x))
-    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+    \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto)
+  apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
 proof -
   fix c :: 'a and x :: 'b
   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -125,7 +125,7 @@
 
 sledgehammer_params [isar_proofs, compress = 1]
 
-lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. \<bar>h x\<bar> <= c * \<bar>f x\<bar>))}"
 by (auto simp add: bigo_def bigo_pos_const)
 
 lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
@@ -160,25 +160,25 @@
 apply (rule subsetI)
 apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
 apply (subst bigo_pos_const [symmetric])+
-apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
+apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> <= \<bar>f n\<bar> then x n else 0" in exI)
 apply (rule conjI)
  apply (rule_tac x = "c + c" in exI)
  apply clarsimp
- apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= (c + c) * \<bar>f xa\<bar>")
   apply (metis mult_2 order_trans)
- apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
   apply (erule order_trans)
   apply (simp add: ring_distribs)
  apply (rule mult_left_mono)
   apply (simp add: abs_triangle_ineq)
  apply (simp add: order_less_le)
-apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
+apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
 apply (rule conjI)
  apply (rule_tac x = "c + c" in exI)
  apply auto
-apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
+apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= (c + c) * \<bar>g xa\<bar>")
  apply (metis order_trans mult_2)
-apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
  apply (erule order_trans)
  apply (simp add: ring_distribs)
 by (metis abs_triangle_ineq mult_le_cancel_left_pos)
@@ -200,9 +200,8 @@
 apply (drule_tac x = "xa" in spec)+
 apply (subgoal_tac "0 <= f xa + g xa")
  apply (simp add: ring_distribs)
- apply (subgoal_tac "abs (a xa + b xa) <= abs (a xa) + abs (b xa)")
-  apply (subgoal_tac "abs (a xa) + abs (b xa) <=
-           max c ca * f xa + max c ca * g xa")
+ apply (subgoal_tac "\<bar>a xa + b xa\<bar> <= \<bar>a xa\<bar> + \<bar>b xa\<bar>")
+  apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> <= max c ca * f xa + max c ca * g xa")
    apply (metis order_trans)
   defer 1
   apply (metis abs_triangle_ineq)
@@ -236,17 +235,17 @@
 by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
           algebra_simps)
 
-lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
+lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
 apply (unfold bigo_def)
 apply auto
 by (metis mult_1 order_refl)
 
-lemma bigo_abs2: "f =o O(\<lambda>x. abs(f x))"
+lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
 apply (unfold bigo_def)
 apply auto
 by (metis mult_1 order_refl)
 
-lemma bigo_abs3: "O(f) = O(\<lambda>x. abs(f x))"
+lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
 proof -
   have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
   have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
@@ -254,15 +253,15 @@
   thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
 qed
 
-lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
+lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
   apply (drule set_plus_imp_minus)
   apply (rule set_minus_imp_plus)
   apply (subst fun_diff_def)
 proof -
   assume a: "f - g : O(h)"
-  have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs(abs (f x) - abs (g x)))"
+  have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
     by (rule bigo_abs2)
-  also have "... <= O(\<lambda>x. abs (f x - g x))"
+  also have "... <= O(\<lambda>x. \<bar>f x - g x\<bar>)"
     apply (rule bigo_elt_subset)
     apply (rule bigo_bounded)
      apply (metis abs_ge_zero)
@@ -274,10 +273,10 @@
     done
   also have "... <= O(h)"
     using a by (rule bigo_elt_subset)
-  finally show "(\<lambda>x. abs (f x) - abs (g x)) : O(h)".
+  finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) : O(h)" .
 qed
 
-lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs(f x)) =o O(g)"
+lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
 by (unfold bigo_def, auto)
 
 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) \<Longrightarrow> O(f) <= O(g) + O(h)"
@@ -285,14 +284,14 @@
   assume "f : g +o O(h)"
   also have "... <= O(g) + O(h)"
     by (auto del: subsetI)
-  also have "... = O(\<lambda>x. abs(g x)) + O(\<lambda>x. abs(h x))"
+  also have "... = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
     by (metis bigo_abs3)
-  also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))"
+  also have "... = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
     by (rule bigo_plus_eq [symmetric], auto)
   finally have "f : ...".
   then have "O(f) <= ..."
     by (elim bigo_elt_subset)
-  also have "... = O(\<lambda>x. abs(g x)) + O(\<lambda>x. abs(h x))"
+  also have "... = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
     by (rule bigo_plus_eq, auto)
   finally show ?thesis
     by (simp add: bigo_abs3 [symmetric])
@@ -307,7 +306,7 @@
 apply (rule_tac x = "c * ca" in exI)
 apply (rule allI)
 apply (erule_tac x = x in allE)+
-apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs(f x)) * (ca * abs (g x))")
+apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
  apply (metis (no_types) abs_ge_zero abs_mult mult_mono')
 by (metis mult.assoc mult.left_commute abs_of_pos mult.left_commute abs_mult)
 
@@ -466,9 +465,9 @@
     simp add: bigo_def elt_set_times_def func_times
     simp del: abs_mult ac_simps)
 (* sledgehammer *)
-  apply (rule_tac x = "ca * (abs c)" in exI)
+  apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
   apply (rule allI)
-  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
+  apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
   apply (erule ssubst)
   apply (subst abs_mult)
   apply (rule mult_left_mono)
@@ -493,10 +492,10 @@
 subsection {* Setsum *}
 
 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
-    \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow>
+    \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
       (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
 apply (auto simp add: bigo_def)
-apply (rule_tac x = "abs c" in exI)
+apply (rule_tac x = "\<bar>c\<bar>" in exI)
 apply (subst abs_of_nonneg) back back
  apply (rule setsum_nonneg)
  apply force
@@ -508,19 +507,19 @@
 by (metis abs_ge_self abs_mult_pos order_trans)
 
 lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
-    \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow>
+    \<exists>c. \<forall>x y. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
       (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
 by (metis (no_types) bigo_setsum_main)
 
 lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
-    \<exists>c. \<forall>y. abs (f y) <= c * (h y) \<Longrightarrow>
+    \<exists>c. \<forall>y. \<bar>f y\<bar> <= c * (h y) \<Longrightarrow>
       (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
 apply (rule bigo_setsum1)
 by metis+
 
 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
     (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
-      O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
+      O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
 apply (rule bigo_setsum1)
  apply (rule allI)+
  apply (rule abs_ge_zero)
@@ -531,7 +530,7 @@
 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
     (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
       (\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
-        O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
+        O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
 apply (rule set_minus_imp_plus)
 apply (subst fun_diff_def)
 apply (subst setsum_subtractf [symmetric])
@@ -544,7 +543,7 @@
       (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
         O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
 apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
-      (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))")
+      (\<lambda>x. SUM y : A x. \<bar>(l x y) * h(k x y)\<bar>)")
  apply (erule ssubst)
  apply (erule bigo_setsum3)
 apply (rule ext)
@@ -616,14 +615,14 @@
 definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
   "f <o g == (\<lambda>x. max (f x - g x) 0)"
 
-lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= abs (f x) \<Longrightarrow>
+lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> <= \<bar>f x\<bar> \<Longrightarrow>
     g =o O(h)"
   apply (unfold bigo_def)
   apply clarsimp
 apply (blast intro: order_trans)
 done
 
-lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= f x \<Longrightarrow>
+lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> <= f x \<Longrightarrow>
       g =o O(h)"
   apply (erule bigo_lesseq1)
 apply (blast intro: abs_ge_self order_trans)
@@ -638,7 +637,7 @@
 done
 
 lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
-    \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= abs (f x) \<Longrightarrow>
+    \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= \<bar>f x\<bar> \<Longrightarrow>
       g =o O(h)"
   apply (erule bigo_lesseq1)
   apply (rule allI)
@@ -703,7 +702,7 @@
 by (auto simp add: func_plus fun_diff_def algebra_simps
     split: split_max abs_split)
 
-lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * abs (h x)"
+lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * \<bar>h x\<bar>"
 apply (simp only: lesso_def bigo_alt_def)
 apply clarsimp
 by (metis add.commute diff_le_eq)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -307,7 +307,7 @@
   proof (intro bcontfunI)
     fix x
     assume "\<And>x. dist (f x) 0 \<le> y"
-    then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
+    then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
       by (metis norm_cmul_rule_thm norm_conv_dist)
   qed (simp add: continuous_intros)
 qed
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -398,7 +398,7 @@
   by transfer (auto simp: algebra_simps setsum_subtractf)
 
 lemma norm_blinfun_of_matrix:
-  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (a i j))"
+  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>a i j\<bar>)"
   apply (rule norm_blinfun_bound)
    apply (simp add: setsum_nonneg)
   apply (simp only: blinfun_of_matrix_apply setsum_left_distrib)
@@ -413,7 +413,7 @@
 proof -
   have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
     using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
-  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (b x i j - a i j))) F"
+  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>b x i j - a i j\<bar>)) F"
     by (auto intro!: Zfun_setsum)
   thus ?thesis
     unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -1473,7 +1473,7 @@
     using kuhn_labelling_lemma[OF *] by blast
   note label = this [rule_format]
   have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
-    abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
+    \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
   proof safe
     fix x y :: 'a
     assume x: "x \<in> unit_cube"
@@ -1481,8 +1481,8 @@
     fix i
     assume i: "label x i \<noteq> label y i" "i \<in> Basis"
     have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
-      abs (fx - x) \<le> abs (fy - fx) + abs (y - x)" by auto
-    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs ((f y - f x)\<bullet>i) + abs ((y - x)\<bullet>i)"
+      \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
+    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
       unfolding inner_simps
       apply (rule *)
       apply (cases "label x i = 0")
@@ -1531,7 +1531,7 @@
   qed
   have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
     norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
-      abs ((f(z) - z)\<bullet>i) < d / (real n)"
+      \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
   proof -
     have d': "d / real n / 8 > 0"
       using d(1) by (simp add: n_def DIM_positive)
@@ -1559,10 +1559,10 @@
         "norm (y - z) < min (e / 2) (d / real n / 8)"
         "label x i \<noteq> label y i"
       assume i: "i \<in> Basis"
-      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) \<le> n1 + n2 \<Longrightarrow>
-        abs (fx - fz) \<le> n3 \<Longrightarrow> abs (x - z) \<le> n4 \<Longrightarrow>
+      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
+        \<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
         n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
-        (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d"
+        (8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
         by auto
       show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
         unfolding inner_simps
@@ -1669,7 +1669,7 @@
                (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
     by (rule kuhn_lemma[OF q1 q2 q3])
   def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
-  have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
+  have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
   proof (rule ccontr)
     have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
       using q(1) b'
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -792,7 +792,7 @@
     dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
 
 
-lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in>UNIV}"
+lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
   by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
 
 lemma component_le_infnorm_cart: "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
@@ -1243,10 +1243,10 @@
 lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
   by (simp add: norm_vec_def)
 
-lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
+lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
   by (simp add: norm_vector_1)
 
-lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
+lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
   by (auto simp add: norm_real dist_norm)
 
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -3862,7 +3862,7 @@
 
 lemma winding_number_big_meets:
   fixes z::complex
-  assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "abs (Re (winding_number \<gamma> z)) \<ge> 1"
+  assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "\<bar>Re (winding_number \<gamma> z)\<bar> \<ge> 1"
       and w: "w \<noteq> z"
   shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
 proof -
@@ -3888,7 +3888,7 @@
   shows
   "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
     \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
-   \<Longrightarrow> abs (Re(winding_number \<gamma> z)) < 1"
+   \<Longrightarrow> \<bar>Re(winding_number \<gamma> z)\<bar> < 1"
    by (auto simp: not_less dest: winding_number_big_meets)
 
 text\<open>One way of proving that WN=1 for a loop.\<close>
@@ -4319,7 +4319,7 @@
   { assume wnz_12: "\<bar>Re (winding_number \<gamma> z)\<bar> > 1/2"
     have "isCont (winding_number \<gamma>) z"
       by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z)
-    then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2"
+    then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < \<bar>Re(winding_number \<gamma> z)\<bar> - 1/2"
       using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast
     def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a"
     have *: "a \<bullet> z' \<le> b - d / 3 * cmod a"
@@ -4479,7 +4479,7 @@
         done
     }
     then have "\<exists>e. 0 < e \<and>
-              (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> abs(t1 - t) < e \<and> abs(t2 - t) < e
+              (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> \<bar>t1 - t\<bar> < e \<and> \<bar>t2 - t\<bar> < e
                 \<longrightarrow> (\<exists>d. 0 < d \<and>
                      (\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
                        (\<forall>u \<in> {0..1}.
@@ -4490,7 +4490,7 @@
   }
   then obtain ee where ee:
        "\<And>t. t \<in> {0..1} \<Longrightarrow> ee t > 0 \<and>
-          (\<forall>t1 t2. t1 \<in> {0..1} \<longrightarrow> t2 \<in> {0..1} \<longrightarrow> abs(t1 - t) < ee t \<longrightarrow> abs(t2 - t) < ee t
+          (\<forall>t1 t2. t1 \<in> {0..1} \<longrightarrow> t2 \<in> {0..1} \<longrightarrow> \<bar>t1 - t\<bar> < ee t \<longrightarrow> \<bar>t2 - t\<bar> < ee t
             \<longrightarrow> (\<exists>d. 0 < d \<and>
                  (\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
                    (\<forall>u \<in> {0..1}.
@@ -4867,7 +4867,7 @@
     with assms show ?thesis by simp
   next
     case 2
-    have [simp]: "abs r = r" using \<open>r > 0\<close> by linarith
+    have [simp]: "\<bar>r\<bar> = r" using \<open>r > 0\<close> by linarith
     have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s"
       by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
     have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
@@ -4940,7 +4940,7 @@
 qed
 
 proposition simple_path_part_circlepath:
-    "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> abs(s - t) \<le> 2*pi)"
+    "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> \<bar>s - t\<bar> \<le> 2*pi)"
 proof (cases "r = 0 \<or> s = t")
   case True
   then show ?thesis
@@ -4952,17 +4952,17 @@
   have *: "\<And>x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z  \<longleftrightarrow> ii*(x - y) * (t - s) = z"
     by (simp add: algebra_simps)
   have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
-                      \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> abs(x - y) \<in> {0,1})"
+                      \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> \<bar>x - y\<bar> \<in> {0,1})"
     by auto
-  have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P(abs(x - y))) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
+  have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
     by force
   have **: "\<And>x y. (\<exists>n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \<longleftrightarrow>
-                  (\<exists>n. abs(x - y) * (t - s) = 2 * (of_int n * pi))"
+                  (\<exists>n. \<bar>x - y\<bar> * (t - s) = 2 * (of_int n * pi))"
     by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
                     intro: exI [where x = "-n" for n])
   have 1: "\<forall>x. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1 \<Longrightarrow> \<bar>s - t\<bar> \<le> 2 * pi"
     apply (rule ccontr)
-    apply (drule_tac x="2*pi / abs(t-s)" in spec)
+    apply (drule_tac x="2*pi / \<bar>t - s\<bar>" in spec)
     using False
     apply (simp add: abs_minus_commute divide_simps)
     apply (frule_tac x=1 in spec)
@@ -4986,7 +4986,7 @@
 qed
 
 proposition arc_part_circlepath:
-  assumes "r \<noteq> 0" "s \<noteq> t" "abs(s - t) < 2*pi"
+  assumes "r \<noteq> 0" "s \<noteq> t" "\<bar>s - t\<bar> < 2*pi"
     shows "arc (part_circlepath z r s t)"
 proof -
   have *: "x = y" if eq: "\<i> * (linepath s t x) = \<i> * (linepath s t y) + 2 * of_int n * complex_of_real pi * \<i>"
@@ -5111,7 +5111,7 @@
 qed
 
 proposition path_image_circlepath [simp]:
-    "path_image (circlepath z r) = sphere z (abs r)"
+    "path_image (circlepath z r) = sphere z \<bar>r\<bar>"
   using path_image_circlepath_minus
   by (force simp add: path_image_circlepath_nonneg abs_if)
 
@@ -6163,7 +6163,7 @@
   with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"]
   obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
     by (auto simp: dist_norm)
-  def R \<equiv> "1 + abs B + norm z"
+  def R \<equiv> "1 + \<bar>B\<bar> + norm z"
   have "R > 0" unfolding R_def by (meson abs_add_one_gt_zero le_less_trans less_add_same_cancel2 norm_ge_zero)
   have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
     apply (rule Cauchy_integral_circlepath)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -8,7 +8,7 @@
 
 lemma cmod_add_real_less:
   assumes "Im z \<noteq> 0" "r\<noteq>0"
-    shows "cmod (z + r) < cmod z + abs r"
+    shows "cmod (z + r) < cmod z + \<bar>r\<bar>"
 proof (cases z)
   case (Complex x y)
   have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
@@ -23,7 +23,7 @@
     done
 qed
 
-lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + abs x"
+lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + \<bar>x\<bar>"
   using cmod_add_real_less [of z "-x"]
   by simp
 
@@ -205,7 +205,7 @@
   finally show ?thesis .
 qed
 
-lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
+lemma exp_complex_eqI: "\<bar>Im w - Im z\<bar> < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
   by (auto simp: exp_eq abs_mult)
 
 lemma exp_integer_2pi:
@@ -361,7 +361,7 @@
   finally show ?thesis .
 qed
 
-lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
+lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
   apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   using cos_double_sin [of "t/2"]
   apply (simp add: real_sqrt_mult)
@@ -579,7 +579,7 @@
 declare power_Suc [simp]
 
 text\<open>32-bit Approximation to e\<close>
-lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
+lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
   using Taylor_exp [of 1 14] exp_le
   apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
   apply (simp only: pos_le_divide_eq [symmetric], linarith)
@@ -1055,14 +1055,14 @@
 
 lemma Re_Ln_pos_lt:
   assumes "z \<noteq> 0"
-    shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
+    shows "\<bar>Im(Ln z)\<bar> < pi/2 \<longleftrightarrow> 0 < Re(z)"
 proof -
   { fix w
     assume "w = Ln z"
     then have w: "Im w \<le> pi" "- pi < Im w"
       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
       by auto
-    then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
+    then have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
       apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
       using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
       apply (simp add: abs_if split: split_if_asm)
@@ -1077,14 +1077,14 @@
 
 lemma Re_Ln_pos_le:
   assumes "z \<noteq> 0"
-    shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
+    shows "\<bar>Im(Ln z)\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
 proof -
   { fix w
     assume "w = Ln z"
     then have w: "Im w \<le> pi" "- pi < Im w"
       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
       by auto
-    then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
+    then have "\<bar>Im w\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
       apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
       using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
       apply (auto simp: abs_if split: split_if_asm)
@@ -1132,7 +1132,7 @@
     by auto
 qed
 
-lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
+lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> \<bar>Im(Ln z)\<bar> < pi/2"
   by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
 
 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
@@ -1834,7 +1834,7 @@
   assumes "\<bar>Re z\<bar> < pi/2"
     shows "Arctan(tan z) = z"
 proof -
-  have ge_pi2: "\<And>n::int. abs (of_int (2*n + 1) * pi/2) \<ge> pi/2"
+  have ge_pi2: "\<And>n::int. \<bar>of_int (2*n + 1) * pi/2\<bar> \<ge> pi/2"
     by (case_tac n rule: int_cases) (auto simp: abs_mult)
   have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
     by (metis distrib_right exp_add mult_2)
@@ -1863,8 +1863,8 @@
 qed
 
 lemma
-  assumes "Re z = 0 \<Longrightarrow> abs(Im z) < 1"
-  shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2"
+  assumes "Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1"
+  shows Re_Arctan_bounds: "\<bar>Re(Arctan z)\<bar> < pi/2"
     and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
 proof -
   have nz0: "1 + \<i>*z \<noteq> 0"
@@ -1889,7 +1889,7 @@
     using assms
     apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
     done
-  show "abs(Re(Arctan z)) < pi/2"
+  show "\<bar>Re(Arctan z)\<bar> < pi/2"
     unfolding Arctan_def divide_complex_def
     using mpi_less_Im_Ln [OF nzi]
     by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def])
@@ -1903,31 +1903,31 @@
     done
 qed
 
-lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable at z"
+lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable at z"
   using has_field_derivative_Arctan
   by (auto simp: complex_differentiable_def)
 
 lemma complex_differentiable_within_Arctan:
-    "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
+    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
   using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
 
 declare has_field_derivative_Arctan [derivative_intros]
 declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
 
 lemma continuous_at_Arctan:
-    "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z) Arctan"
+    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z) Arctan"
   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
 
 lemma continuous_within_Arctan:
-    "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z within s) Arctan"
+    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arctan"
   using continuous_at_Arctan continuous_at_imp_continuous_within by blast
 
 lemma continuous_on_Arctan [continuous_intros]:
-    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
+    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
   by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
 
 lemma holomorphic_on_Arctan:
-    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
+    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
   by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
 
 
@@ -1988,17 +1988,17 @@
 lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
   by (metis arctan_less_iff arctan_minus arctan_one)
 
-lemma arctan_less_pi4: "abs x < 1 \<Longrightarrow> abs(arctan x) < pi/4"
+lemma arctan_less_pi4: "\<bar>x\<bar> < 1 \<Longrightarrow> \<bar>arctan x\<bar> < pi/4"
   by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
 
-lemma arctan_le_pi4: "abs x \<le> 1 \<Longrightarrow> abs(arctan x) \<le> pi/4"
+lemma arctan_le_pi4: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>arctan x\<bar> \<le> pi/4"
   by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one)
 
-lemma abs_arctan: "abs(arctan x) = arctan(abs x)"
+lemma abs_arctan: "\<bar>arctan x\<bar> = arctan \<bar>x\<bar>"
   by (simp add: abs_if arctan_minus)
 
 lemma arctan_add_raw:
-  assumes "abs(arctan x + arctan y) < pi/2"
+  assumes "\<bar>arctan x + arctan y\<bar> < pi/2"
     shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))"
 proof (rule arctan_unique [symmetric])
   show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
@@ -2027,7 +2027,7 @@
 qed
 
 lemma arctan_add_small:
-  assumes "abs(x * y) < 1"
+  assumes "\<bar>x * y\<bar> < 1"
     shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))"
 proof (cases "x = 0 \<or> y = 0")
   case True then show ?thesis
@@ -2044,7 +2044,7 @@
 qed
 
 lemma abs_arctan_le:
-  fixes x::real shows "abs(arctan x) \<le> abs x"
+  fixes x::real shows "\<bar>arctan x\<bar> \<le> \<bar>x\<bar>"
 proof -
   { fix w::complex and z::complex
     assume *: "w \<in> \<real>" "z \<in> \<real>"
@@ -2064,7 +2064,7 @@
 lemma arctan_le_self: "0 \<le> x \<Longrightarrow> arctan x \<le> x"
   by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
 
-lemma abs_tan_ge: "abs x < pi/2 \<Longrightarrow> abs x \<le> abs(tan x)"
+lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>"
   by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
 
 
@@ -2078,7 +2078,7 @@
   apply auto
   by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral)
 
-lemma Arcsin_range_lemma: "abs (Re z) < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
+lemma Arcsin_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
   using Complex.cmod_power2 [of z, symmetric]
   by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus)
 
@@ -2393,7 +2393,7 @@
 
 subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
 
-lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
+lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> \<bar>Re(Arcsin z)\<bar> < pi/2"
   unfolding Re_Arcsin
   by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
 
@@ -2405,14 +2405,14 @@
   unfolding Re_Arccos
   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
 
-lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
+lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
   by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
 
 lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   unfolding Re_Arcsin
   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
 
-lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
+lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
   by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
 
 
@@ -2521,7 +2521,7 @@
 subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
 
 lemma Im_Arcsin_of_real:
-  assumes "abs x \<le> 1"
+  assumes "\<bar>x\<bar> \<le> 1"
     shows "Im (Arcsin (of_real x)) = 0"
 proof -
   have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
@@ -2539,7 +2539,7 @@
   by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
 
 lemma arcsin_eq_Re_Arcsin:
-  assumes "abs x \<le> 1"
+  assumes "\<bar>x\<bar> \<le> 1"
     shows "arcsin x = Re (Arcsin (of_real x))"
 unfolding arcsin_def
 proof (rule the_equality, safe)
@@ -2564,14 +2564,14 @@
     done
 qed
 
-lemma of_real_arcsin: "abs x \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
+lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
   by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
 
 
 subsection\<open>Relationship with Arccos on the Real Numbers\<close>
 
 lemma Im_Arccos_of_real:
-  assumes "abs x \<le> 1"
+  assumes "\<bar>x\<bar> \<le> 1"
     shows "Im (Arccos (of_real x)) = 0"
 proof -
   have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
@@ -2589,7 +2589,7 @@
   by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
 
 lemma arccos_eq_Re_Arccos:
-  assumes "abs x \<le> 1"
+  assumes "\<bar>x\<bar> \<le> 1"
     shows "arccos x = Re (Arccos (of_real x))"
 unfolding arccos_def
 proof (rule the_equality, safe)
@@ -2614,7 +2614,7 @@
     done
 qed
 
-lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
+lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
   by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
 
 subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -3328,13 +3328,13 @@
     ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x \<in> affine hull S"
       using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"]
       by (simp add: algebra_simps)
-    have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
+    have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
       unfolding dist_norm norm_scaleR[symmetric]
       apply (rule arg_cong[where f=norm])
       using \<open>e > 0\<close>
       apply (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
       done
-    also have "\<dots> = abs (1/e) * norm (x - e *\<^sub>R (x - c) - y)"
+    also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
       by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
     also have "\<dots> < d"
       using as[unfolded dist_norm] and \<open>e > 0\<close>
@@ -6076,15 +6076,15 @@
   fixes s :: "('a::real_normed_vector) set"
   assumes "open s"
     and "convex_on s f"
-    and "\<forall>x\<in>s. abs(f x) \<le> b"
+    and "\<forall>x\<in>s. \<bar>f x\<bar> \<le> b"
   shows "continuous_on s f"
   apply (rule continuous_at_imp_continuous_on)
   unfolding continuous_at_real_range
 proof (rule,rule,rule)
   fix x and e :: real
   assume "x \<in> s" "e > 0"
-  def B \<equiv> "abs b + 1"
-  have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> abs (f x) \<le> B"
+  def B \<equiv> "\<bar>b\<bar> + 1"
+  have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> \<bar>f x\<bar> \<le> B"
     unfolding B_def
     defer
     apply (drule assms(3)[rule_format])
@@ -6193,7 +6193,7 @@
   fixes x :: "'a::real_normed_vector"
   assumes "convex_on (cball x e) f"
     and "\<forall>y \<in> cball x e. f y \<le> b"
-  shows "\<forall>y \<in> cball x e. abs (f y) \<le> b + 2 * abs (f x)"
+  shows "\<forall>y \<in> cball x e. \<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
   apply rule
 proof (cases "0 \<le> e")
   case True
@@ -6310,7 +6310,7 @@
     apply (rule e(1))
     apply (rule dsube)
     done
-  then have "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)"
+  then have "\<forall>y\<in>cball x d. \<bar>f y\<bar> \<le> k + 2 * \<bar>f x\<bar>"
     apply (rule convex_bounds_lemma)
     apply (rule ballI)
     apply (rule k [rule_format])
@@ -6751,13 +6751,13 @@
     assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d"
     have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
       using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
-    have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
+    have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
       unfolding dist_norm
       unfolding norm_scaleR[symmetric]
       apply (rule arg_cong[where f=norm])
       using \<open>e > 0\<close>
       by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
-    also have "\<dots> = abs (1/e) * norm (x - e *\<^sub>R (x - c) - y)"
+    also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
       by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
     also have "\<dots> < d"
       using as[unfolded dist_norm] and \<open>e > 0\<close>
@@ -7001,7 +7001,7 @@
     proof (rule setsum_mono)
       fix i :: 'a
       assume i: "i \<in> Basis"
-      then have "abs (y\<bullet>i - x\<bullet>i) < ?d"
+      then have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d"
         apply -
         apply (rule le_less_trans)
         using Basis_le_norm[OF i, of "y - x"]
@@ -7186,7 +7186,7 @@
           assume "i \<in> d"
           with d have i: "i \<in> Basis"
             by auto
-          have "abs (y\<bullet>i - x\<bullet>i) < ?d"
+          have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d"
             apply (rule le_less_trans)
             using Basis_le_norm[OF i, of "y - x"]
             using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
@@ -9860,7 +9860,7 @@
 lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
   by (simp add: setdist_def)
 
-lemma setdist_Lipschitz: "abs(setdist {x} s - setdist {y} s) \<le> dist x y"
+lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"
   apply (subst setdist_singletons [symmetric])
   by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -372,7 +372,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_derivative f') (at x within s)"
     and "(f has_derivative f'') (at x within s)"
-    and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < abs d \<and> abs d < e \<and> (x + d *\<^sub>R i) \<in> s"
+    and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> s"
   shows "f' = f''"
 proof -
   note as = assms(1,2)[unfolded has_derivative_def]
@@ -415,9 +415,9 @@
     obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
       using assms(3) i d(1) by blast
     have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
-        norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
+        norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
       unfolding scaleR_right_distrib by auto
-    also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
+    also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
       unfolding f'.scaleR f''.scaleR
       unfolding scaleR_right_distrib scaleR_minus_right
       by auto
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -82,19 +82,19 @@
 
 lemma infnorm_2:
   fixes x :: "real^2"
-  shows "infnorm x = max (abs (x$1)) (abs (x$2))"
+  shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
   unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
 
 lemma infnorm_eq_1_2:
   fixes x :: "real^2"
   shows "infnorm x = 1 \<longleftrightarrow>
-    abs (x$1) \<le> 1 \<and> abs (x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
+    \<bar>x$1\<bar> \<le> 1 \<and> \<bar>x$2\<bar> \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
   unfolding infnorm_2 by auto
 
 lemma infnorm_eq_1_imp:
   fixes x :: "real^2"
   assumes "infnorm x = 1"
-  shows "abs (x$1) \<le> 1" and "abs (x$2) \<le> 1"
+  shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
   using assms unfolding infnorm_eq_1_2 by auto
 
 lemma fashoda_unit:
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -499,7 +499,7 @@
 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
   by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
 
-lemma abs_eq_content: "abs (y - x) = (if x\<le>y then content {x .. y} else content {y..x})"
+lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
   by (auto simp: content_real)
 
 lemma content_singleton[simp]: "content {a} = 0"
@@ -2116,7 +2116,7 @@
     proof (rule exI [where x=n], clarify)
       fix x y
       assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
-      have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis"
+      have "dist x y \<le> setsum (\<lambda>i. \<bar>(x - y)\<bullet>i\<bar>) Basis"
         unfolding dist_norm by(rule norm_le_l1)
       also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
       proof (rule setsum_mono)
@@ -3140,7 +3140,7 @@
        apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
        apply (simp add: interval_split[symmetric] k)
        done
-  let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x (abs(x\<bullet>k - c)) \<inter> d1 x \<inter> d2 x"
+  let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x \<bar>x\<bullet>k - c\<bar> \<inter> d1 x \<inter> d2 x"
   have "gauge ?d"
     using d1 d2 unfolding gauge_def by auto
   then show ?case
@@ -4659,11 +4659,11 @@
 lemma interval_doublesplit:
   fixes a :: "'a::euclidean_space"
   assumes "k \<in> Basis"
-  shows "cbox a b \<inter> {x . abs(x\<bullet>k - c) \<le> (e::real)} =
+  shows "cbox a b \<inter> {x . \<bar>x\<bullet>k - c\<bar> \<le> (e::real)} =
     cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) (c - e) else a\<bullet>i) *\<^sub>R i)
      (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) (c + e) else b\<bullet>i) *\<^sub>R i)"
 proof -
-  have *: "\<And>x c e::real. abs(x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
+  have *: "\<And>x c e::real. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
     by auto
   have **: "\<And>s P Q. s \<inter> {x. P x \<and> Q x} = (s \<inter> {x. Q x}) \<inter> {x. P x}"
     by blast
@@ -4675,10 +4675,10 @@
   fixes a :: "'a::euclidean_space"
   assumes "p division_of (cbox a b)"
     and k: "k \<in> Basis"
-  shows "{l \<inter> {x. abs(x\<bullet>k - c) \<le> e} |l. l \<in> p \<and> l \<inter> {x. abs(x\<bullet>k - c) \<le> e} \<noteq> {}}
-         division_of  (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> e})"
-proof -
-  have *: "\<And>x c. abs (x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
+  shows "{l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} |l. l \<in> p \<and> l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
+         division_of  (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
+proof -
+  have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
     by auto
   have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
     by auto
@@ -4700,7 +4700,7 @@
   fixes a :: "'a::euclidean_space"
   assumes "0 < e"
     and k: "k \<in> Basis"
-  obtains d where "0 < d" and "content (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> d}) < e"
+  obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
 proof (cases "content (cbox a b) = 0")
   case True
   then have ce: "content (cbox a b) < e"
@@ -4780,7 +4780,7 @@
     fix p
     assume p: "p tagged_division_of (cbox a b) \<and> (\<lambda>x. ball x d) fine p"
     have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
-      (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. abs(x\<bullet>k - c) \<le> d}) *\<^sub>R ?i x)"
+      (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
       apply (rule setsum.cong)
       apply (rule refl)
       unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
@@ -6695,7 +6695,7 @@
 
 lemma content_image_affinity_cbox:
   "content((\<lambda>x::'a::euclidean_space. m *\<^sub>R x + c) ` cbox a b) =
-    abs m ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
+    \<bar>m\<bar> ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
 proof -
   {
     presume *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
@@ -6743,7 +6743,7 @@
   fixes a :: "'a::euclidean_space"
   assumes "(f has_integral i) (cbox a b)"
       and "m \<noteq> 0"
-  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
+  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (\<bar>m\<bar> ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
   apply (rule has_integral_twiddle)
   using assms
   apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox)
@@ -6807,7 +6807,7 @@
 
 lemma content_image_stretch_interval:
   "content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
-    abs (setprod m Basis) * content (cbox a b)"
+    \<bar>setprod m Basis\<bar> * content (cbox a b)"
 proof (cases "cbox a b = {}")
   case True
   then show ?thesis
@@ -6847,7 +6847,7 @@
   assumes "(f has_integral i) (cbox a b)"
     and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
-    ((1/(abs(setprod m Basis))) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+    ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
   apply (rule has_integral_twiddle[where f=f])
   unfolding zero_less_abs_iff content_image_stretch_interval
   unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
@@ -8829,8 +8829,8 @@
     unfolding fine_inter
   proof (safe, goal_cases)
     have **: "\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
-      abs (i - j) < e / 3 \<Longrightarrow> abs (g2 - i) < e / 3 \<Longrightarrow>  abs (g1 - i) < e / 3 \<Longrightarrow>
-      abs (h2 - j) < e / 3 \<Longrightarrow> abs (h1 - j) < e / 3 \<Longrightarrow> abs (f1 - f2) < e"
+      \<bar>i - j\<bar> < e / 3 \<Longrightarrow> \<bar>g2 - i\<bar> < e / 3 \<Longrightarrow> \<bar>g1 - i\<bar> < e / 3 \<Longrightarrow>
+      \<bar>h2 - j\<bar> < e / 3 \<Longrightarrow> \<bar>h1 - j\<bar> < e / 3 \<Longrightarrow> \<bar>f1 - f2\<bar> < e"
     using \<open>e > 0\<close> by arith
     case prems: (1 p1 p2)
     note tagged_division_ofD(2-4) note * = this[OF prems(1)] this[OF prems(4)]
@@ -8996,9 +8996,9 @@
       have **: "ball 0 B1 \<subseteq> ball (0::'n) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n) (max B1 B2)"
         by auto
       have *: "\<And>ga gc ha hc fa fc::real.
-        abs (ga - i) < e / 3 \<and> abs (gc - i) < e / 3 \<and> abs (ha - j) < e / 3 \<and>
-        abs (hc - j) < e / 3 \<and> abs (i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow>
-        abs (fa - fc) < e"
+        \<bar>ga - i\<bar> < e / 3 \<and> \<bar>gc - i\<bar> < e / 3 \<and> \<bar>ha - j\<bar> < e / 3 \<and>
+        \<bar>hc - j\<bar> < e / 3 \<and> \<bar>i - j\<bar> < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow>
+        \<bar>fa - fc\<bar> < e"
         by (simp add: abs_real_def split: split_if_asm)
       show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d)
         (\<lambda>x. if x \<in> s then f x else 0)) < e"
@@ -9875,7 +9875,7 @@
         case 3
         note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
         have *: "\<And>sr sx ss ks kr::real. kr = sr \<longrightarrow> ks = ss \<longrightarrow>
-          ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i\<bullet>1 - kr\<bullet>1 \<and> i\<bullet>1 - kr\<bullet>1 < e/4 \<longrightarrow> abs (sx - i) < e/4"
+          ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i\<bullet>1 - kr\<bullet>1 \<and> i\<bullet>1 - kr\<bullet>1 < e/4 \<longrightarrow> \<bar>sx - i\<bar> < e/4"
           by auto
         show ?case
           unfolding real_norm_def
@@ -10087,8 +10087,8 @@
           apply (subst norm_minus_commute)
           apply auto
           done
-        have *: "\<And>f1 f2 g. abs (f1 - i) < e / 2 \<longrightarrow> abs (f2 - g) < e / 2 \<longrightarrow>
-          f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> abs (g - i) < e"
+        have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e / 2 \<longrightarrow> \<bar>f2 - g\<bar> < e / 2 \<longrightarrow>
+          f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e"
           unfolding real_inner_1_right by arith
         show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0) - i) < e"
           unfolding real_norm_def
@@ -10305,7 +10305,7 @@
     done
   have norm: "norm ig < dia + e"
     if "norm sg \<le> dsa"
-    and "abs (dsa - dia) < e / 2"
+    and "\<bar>dsa - dia\<bar> < e / 2"
     and "norm (sg - ig) < e / 2"
     for e dsa dia and sg ig :: 'a
     apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
@@ -10445,7 +10445,7 @@
     (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
   unfolding absolutely_integrable_on_def
   using integrable_cmul[of f s c]
-  using integrable_cmul[of "\<lambda>x. norm (f x)" s "abs c"]
+  using integrable_cmul[of "\<lambda>x. norm (f x)" s "\<bar>c\<bar>"]
   by auto
 
 lemma absolutely_integrable_neg[intro]:
@@ -10463,7 +10463,7 @@
 
 lemma absolutely_integrable_abs[intro]:
   "f absolutely_integrable_on s \<Longrightarrow>
-    (\<lambda>x. abs(f x::real)) absolutely_integrable_on s"
+    (\<lambda>x. \<bar>f x::real\<bar>) absolutely_integrable_on s"
   apply (drule absolutely_integrable_norm)
   unfolding real_norm_def
   apply assumption
@@ -10510,7 +10510,7 @@
 lemma helplemma:
   assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
     and "finite s"
-  shows "abs (setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s) < e"
+  shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
   unfolding setsum_subtractf[symmetric]
   apply (rule le_less_trans[OF setsum_abs])
   apply (rule le_less_trans[OF _ assms(1)])
@@ -10709,8 +10709,8 @@
         done
       note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
 
-      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
-        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
+      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
+        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
         by arith
       show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
         unfolding real_norm_def
@@ -11061,7 +11061,7 @@
     proof -
       fix a b :: 'n
       assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
-      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
+      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
         by arith
       show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
         unfolding real_norm_def
@@ -11121,8 +11121,8 @@
           p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
           by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
             (auto simp add: fine_inter)
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
-          abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
+          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
           by arith
         show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
           apply (subst if_P)
@@ -11136,7 +11136,7 @@
             unfolding tagged_division_of_def split_def
             apply auto
             done
-          show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))) < e / 2"
+          show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
             using d1(2)[rule_format,OF conjI[OF p(1,2)]]
             by (simp only: real_norm_def)
           show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
@@ -11295,7 +11295,7 @@
   fixes f :: "'a::euclidean_space => 'b::euclidean_space"
     and T :: "'c::euclidean_space \<Rightarrow> 'b"
   assumes f: "f absolutely_integrable_on s"
-  shows "(\<lambda>x. (\<Sum>i\<in>Basis. abs(f x\<bullet>T i) *\<^sub>R i)) absolutely_integrable_on s"
+  shows "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>T i\<bar> *\<^sub>R i)) absolutely_integrable_on s"
   (is "?Tf absolutely_integrable_on s")
 proof -
   have if_distrib: "\<And>P A B x. (if P then A else B) *\<^sub>R x = (if P then A *\<^sub>R x else B *\<^sub>R x)"
@@ -11350,7 +11350,7 @@
 lemma absolutely_integrable_abs_eq:
   fixes f::"'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
-    (\<lambda>x. (\<Sum>i\<in>Basis. abs(f x\<bullet>i) *\<^sub>R i)::'m) integrable_on s"
+    (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on s"
   (is "?l = ?r")
 proof
   assume ?l
@@ -11976,7 +11976,7 @@
         apply safe
       proof goal_cases
         case prems: (1 n)
-        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
+        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> \<bar>ix - Inf ?S\<bar> < r"
           by arith
         show ?case
           unfolding real_norm_def
@@ -12046,7 +12046,7 @@
         apply safe
       proof goal_cases
         case prems: (1 n)
-        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
+        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> \<bar>ix - Sup ?S\<bar> < r"
           by arith
         show ?case
           apply simp
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -13,7 +13,7 @@
   assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
   assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
   assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
-  assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
+  assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
 begin
 
 subclass order
@@ -55,7 +55,7 @@
   and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
   using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
 
-lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
+lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
   by (auto simp: eucl_abs)
 
 lemma
@@ -159,12 +159,13 @@
   shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
   by (cases i) (auto simp: Basis_prod_def)
 
-instantiation prod::(abs, abs) abs
+instantiation prod :: (abs, abs) abs
 begin
 
-definition "abs x = (abs (fst x), abs (snd x))"
+definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
 
-instance proof qed
+instance ..
+
 end
 
 instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
@@ -269,7 +270,7 @@
 definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
 definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
 definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
-definition "abs x = (\<chi> i. abs (x $ i))"
+definition "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
 
 instance
   apply standard
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -169,7 +169,7 @@
     qed
 qed
 
-lemma norm_lemma_xy: "\<lbrakk>abs b + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
+lemma norm_lemma_xy: "\<lbrakk>\<bar>b\<bar> + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
   by (metis abs_add_one_not_less_self add.commute diff_le_eq dual_order.trans le_less_linear
          norm_diff_ineq)
 
@@ -196,7 +196,7 @@
       by auto
     show ?thesis
     unfolding eventually_at_infinity
-    proof (rule exI [where x="max M (max 1 ((abs B + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
+    proof (rule exI [where x="max M (max 1 ((\<bar>B\<bar> + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
       fix z::'a
       assume les: "M \<le> norm z"  "1 \<le> norm z"  "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z"
       then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -3201,7 +3201,7 @@
   by (simp add: bounded_iff bdd_above_def)
 
 lemma bounded_realI:
-  assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
+  assumes "\<forall>x\<in>s. \<bar>x::real\<bar> \<le> B"
   shows "bounded s"
   unfolding bounded_def dist_real_def
   by (metis abs_minus_commute assms diff_0_right)
@@ -3275,7 +3275,7 @@
 
 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)"
   apply (simp add: bounded_iff)
-  apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x \<le> y \<longrightarrow> x \<le> 1 + abs y)")
+  apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)")
   apply metis
   apply arith
   done
@@ -5905,7 +5905,7 @@
     then obtain e where "e>0"
       and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
       by auto
-    have "e * abs c > 0"
+    have "e * \<bar>c\<bar> > 0"
       using assms(1)[unfolded zero_less_abs_iff[symmetric]] \<open>e>0\<close> by auto
     moreover
     {
@@ -5923,7 +5923,7 @@
         by auto
     }
     ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> op *\<^sub>R c ` s"
-      apply (rule_tac x="e * abs c" in exI)
+      apply (rule_tac x="e * \<bar>c\<bar>" in exI)
       apply auto
       done
   }
@@ -6221,22 +6221,22 @@
 
 lemma open_real:
   fixes s :: "real set"
-  shows "open s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)"
+  shows "open s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. \<bar>x' - x\<bar> < e --> x' \<in> s)"
   unfolding open_dist dist_norm by simp
 
 lemma islimpt_approachable_real:
   fixes s :: "real set"
-  shows "x islimpt s \<longleftrightarrow> (\<forall>e>0.  \<exists>x'\<in> s. x' \<noteq> x \<and> abs(x' - x) < e)"
+  shows "x islimpt s \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> s. x' \<noteq> x \<and> \<bar>x' - x\<bar> < e)"
   unfolding islimpt_approachable dist_norm by simp
 
 lemma closed_real:
   fixes s :: "real set"
-  shows "closed s \<longleftrightarrow> (\<forall>x. (\<forall>e>0.  \<exists>x' \<in> s. x' \<noteq> x \<and> abs(x' - x) < e) \<longrightarrow> x \<in> s)"
+  shows "closed s \<longleftrightarrow> (\<forall>x. (\<forall>e>0.  \<exists>x' \<in> s. x' \<noteq> x \<and> \<bar>x' - x\<bar> < e) \<longrightarrow> x \<in> s)"
   unfolding closed_limpt islimpt_approachable dist_norm by simp
 
 lemma continuous_at_real_range:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
-  shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
+  shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"
   unfolding continuous_at
   unfolding Lim_at
   unfolding dist_nz[symmetric]
@@ -6255,7 +6255,7 @@
 lemma continuous_on_real_range:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
   shows "continuous_on s f \<longleftrightarrow>
-    (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> abs(f x' - f x) < e))"
+    (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
   unfolding continuous_on_iff dist_norm by simp
 
 text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -65,7 +65,7 @@
   fixes f :: "real \<Rightarrow> real"
   assumes contf: "continuous_on {0..1} f" and e: "0 < e"
     shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1}
-                    \<longrightarrow> abs(f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)) < e"
+                    \<longrightarrow> \<bar>f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)\<bar> < e"
 proof -
   have "bounded (f ` {0..1})"
     using compact_continuous_image compact_imp_bounded contf by blast
@@ -110,7 +110,7 @@
       assume k: "k \<le> n"
       then have kn: "0 \<le> k / n" "k / n \<le> 1"
         by (auto simp: divide_simps)
-      consider (lessd) "abs(x - k / n) < d" | (ged) "d \<le> abs(x - k / n)"
+      consider (lessd) "\<bar>x - k / n\<bar> < d" | (ged) "d \<le> \<bar>x - k / n\<bar>"
         by linarith
       then have "\<bar>(f x - f (k/n))\<bar> \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
       proof cases
@@ -758,7 +758,7 @@
           "\<And>x y. x \<in> s \<and> y \<in> s \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)"
           "continuous_on s f"
        "0 < e"
-    shows "\<exists>g. P(g) \<and> (\<forall>x \<in> s. abs(f x - g x) < e)"
+    shows "\<exists>g. P(g) \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)"
 proof -
   interpret PR: function_ring_on "Collect P"
     apply unfold_locales
@@ -1081,7 +1081,7 @@
 lemma Stone_Weierstrass_real_polynomial_function:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
   assumes "compact s" "continuous_on s f" "0 < e"
-    shows "\<exists>g. real_polynomial_function g \<and> (\<forall>x \<in> s. abs(f x - g x) < e)"
+    shows "\<exists>g. real_polynomial_function g \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)"
 proof -
   interpret PR: function_ring_on "Collect real_polynomial_function"
     apply unfold_locales
@@ -1102,14 +1102,14 @@
 proof -
   { fix b :: 'b
     assume "b \<in> Basis"
-    have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> s. abs(f x \<bullet> b - p x) < e / DIM('b))"
+    have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
       apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF s _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]])
       using e f
       apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros)
       done
   }
   then obtain pf where pf:
-      "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> s. abs(f x \<bullet> b - pf b x) < e / DIM('b))"
+      "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - pf b x\<bar> < e / DIM('b))"
       apply (rule bchoice [rule_format, THEN exE])
       apply assumption
       apply (force simp add: intro: that)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/ex/Approximations.thy
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -24,7 +24,7 @@
 qed
 
 (*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*)
-lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)"
+lemma pi_approx_32: "\<bar>pi - 13493037705/4294967296\<bar> \<le> inverse(2 ^ 32)"
   apply (simp only: abs_diff_le_iff)
   apply (rule sin_pi6_straddle, simp_all)
    using Taylor_sin [of "1686629713/3221225472" 11]
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/HLog.thy
--- a/src/HOL/NSA/HLog.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HLog.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -117,7 +117,7 @@
 
 lemma hlog_hrabs_HInfinite_Infinitesimal:
      "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
-      ==> hlog a (abs x) : Infinitesimal"
+      ==> hlog a \<bar>x\<bar> : Infinitesimal"
 apply (frule HInfinite_gt_zero_gt_one)
 apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
             HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/HSeries.thy
--- a/src/HOL/NSA/HSeries.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HSeries.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -68,7 +68,7 @@
 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
 by (drule_tac f = f in sumhr_split_add [symmetric], simp)
 
-lemma sumhr_hrabs: "!!m n. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
+lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
 unfolding sumhr_app by transfer (rule setsum_abs)
 
 text{* other general version also needed *}
@@ -130,7 +130,7 @@
 unfolding sumhr_app by transfer (rule refl)
 
 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
-      ==> abs (sumhr(M, N, f)) @= 0"
+      ==> \<bar>sumhr(M, N, f)\<bar> @= 0"
 apply (cut_tac x = M and y = N in linorder_less_linear)
 apply (auto simp add: approx_refl)
 apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
@@ -167,7 +167,7 @@
 
 lemma NSsummable_NSCauchy:
      "NSsummable f =
-      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
+      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> @= 0)"
 apply (auto simp add: summable_NSsummable_iff [symmetric]
        summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
        NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
@@ -189,14 +189,14 @@
 
 text{*Nonstandard comparison test*}
 lemma NSsummable_comparison_test:
-     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
+     "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
 apply (fold summable_NSsummable_iff)
 apply (rule summable_comparison_test, simp, assumption)
 done
 
 lemma NSsummable_rabs_comparison_test:
-     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
-      ==> NSsummable (%k. abs (f k))"
+     "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |]
+      ==> NSsummable (%k. \<bar>f k\<bar>)"
 apply (rule NSsummable_comparison_test)
 apply (auto)
 done
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -103,14 +103,14 @@
 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
 
-lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = abs(x)"
+lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
 by (transfer, simp)
 
-lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
+lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
 by (transfer, simp)
 
 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
-     "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
+     "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
 by (transfer, simp)
 
 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -216,8 +216,7 @@
 lemma star_n_one_num: "1 = star_n (%n. 1)"
 by (simp only: star_one_def star_of_def)
 
-lemma star_n_abs:
-     "abs (star_n X) = star_n (%n. abs (X n))"
+lemma star_n_abs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
 by (simp only: star_abs_def starfun_star_n)
 
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
@@ -280,17 +279,16 @@
 
 subsection{*Absolute Value Function for the Hyperreals*}
 
-lemma hrabs_add_less:
-     "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
+lemma hrabs_add_less: "[| \<bar>x\<bar> < r; \<bar>y\<bar> < s |] ==> \<bar>x + y\<bar> < r + (s::hypreal)"
 by (simp add: abs_if split: split_if_asm)
 
-lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
+lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r ==> (0::hypreal) < r"
 by (blast intro!: order_le_less_trans abs_ge_zero)
 
-lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x"
+lemma hrabs_disj: "\<bar>x\<bar> = (x::'a::abs_if) \<or> \<bar>x\<bar> = -x"
 by (simp add: abs_if)
 
-lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
+lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = \<bar>x + - z\<bar> ==> y = z | x = y"
 by (simp add: abs_if split add: split_if_asm)
 
 
@@ -364,8 +362,7 @@
 
 (*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
   result proved in Rings or Fields*)
-lemma hrabs_hrealpow_two [simp]:
-     "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
+lemma hrabs_hrealpow_two [simp]: "\<bar>x ^ Suc (Suc 0)\<bar> = (x::hypreal) ^ Suc (Suc 0)"
 by (simp add: abs_mult)
 
 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
@@ -427,7 +424,7 @@
 by transfer (rule power_inverse [symmetric])
 
 lemma hyperpow_hrabs:
-  "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
+  "\<And>r n. \<bar>r::'a::{linordered_idom} star\<bar> pow n = \<bar>r pow n\<bar>"
 by transfer (rule power_abs [symmetric])
 
 lemma hyperpow_add:
@@ -460,7 +457,7 @@
 by transfer (rule power_one)
 
 lemma hrabs_hyperpow_minus [simp]:
-  "\<And>(a::'a::{linordered_idom} star) n. abs((-a) pow n) = abs (a pow n)"
+  "\<And>(a::'a::{linordered_idom} star) n. \<bar>(-a) pow n\<bar> = \<bar>a pow n\<bar>"
 by transfer (rule abs_power_minus)
 
 lemma hyperpow_mult:
@@ -473,12 +470,12 @@
 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
 lemma hrabs_hyperpow_two [simp]:
-  "abs(x pow 2) =
+  "\<bar>x pow 2\<bar> =
    (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
 by (simp only: abs_of_nonneg hyperpow_two_le)
 
 lemma hyperpow_two_hrabs [simp]:
-  "abs(x::'a::{linordered_idom} star) pow 2 = x pow 2"
+  "\<bar>x::'a::{linordered_idom} star\<bar> pow 2 = x pow 2"
 by (simp add: hyperpow_hrabs)
 
 text{*The precondition could be weakened to @{term "0\<le>x"}*}
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/NSA.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -181,7 +181,7 @@
 lemma Reals_add_cancel: "\<lbrakk>x + y \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> x \<in> \<real>"
 by (drule (1) Reals_diff, simp)
 
-lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> abs x \<in> \<real>"
+lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> \<bar>x\<bar> \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
 lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>"
@@ -280,7 +280,7 @@
 lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
 by (simp add: HFinite_def)
 
-lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
+lemma HFinite_hrabs_iff [iff]: "(\<bar>x::hypreal\<bar> \<in> HFinite) = (x \<in> HFinite)"
 by (simp add: HFinite_def)
 
 lemma HFinite_hnorm_iff [iff]:
@@ -355,7 +355,7 @@
 by (simp add: Infinitesimal_def)
 
 lemma Infinitesimal_hrabs_iff [iff]:
-  "(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+  "(\<bar>x::hypreal\<bar> \<in> Infinitesimal) = (x \<in> Infinitesimal)"
 by (simp add: abs_if)
 
 lemma Infinitesimal_of_hypreal_iff [simp]:
@@ -509,7 +509,7 @@
 by auto
 
 lemma HFinite_diff_Infinitesimal_hrabs:
-  "(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
+  "(x::hypreal) \<in> HFinite - Infinitesimal ==> \<bar>x\<bar> \<in> HFinite - Infinitesimal"
 by blast
 
 lemma hnorm_le_Infinitesimal:
@@ -521,11 +521,11 @@
 by (erule hnorm_le_Infinitesimal, erule order_less_imp_le)
 
 lemma hrabs_le_Infinitesimal:
-     "[| e \<in> Infinitesimal; abs (x::hypreal) \<le> e |] ==> x \<in> Infinitesimal"
+     "[| e \<in> Infinitesimal; \<bar>x::hypreal\<bar> \<le> e |] ==> x \<in> Infinitesimal"
 by (erule hnorm_le_Infinitesimal, simp)
 
 lemma hrabs_less_Infinitesimal:
-      "[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal"
+      "[| e \<in> Infinitesimal; \<bar>x::hypreal\<bar> < e |] ==> x \<in> Infinitesimal"
 by (erule hnorm_less_Infinitesimal, simp)
 
 lemma Infinitesimal_interval:
@@ -540,7 +540,7 @@
 
 
 lemma lemma_Infinitesimal_hyperpow:
-     "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
+     "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> \<bar>x pow N\<bar> \<le> \<bar>x\<bar>"
 apply (unfold Infinitesimal_def)
 apply (auto intro!: hyperpow_Suc_le_self2
           simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
@@ -1239,7 +1239,7 @@
      "[| (x::hypreal) \<in> HFinite;
          isLub \<real> {s. s \<in> \<real> & s < x} t;
          r \<in> \<real>; 0 < r |]
-      ==> abs (x - t) < r"
+      ==> \<bar>x - t\<bar> < r"
 apply (frule lemma_st_part1a)
 apply (frule_tac [4] lemma_st_part2a, auto)
 apply (drule order_le_imp_less_or_eq)+
@@ -1250,7 +1250,7 @@
 
 lemma lemma_st_part_major2:
      "[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t |]
-      ==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
+      ==> \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
 by (blast dest!: lemma_st_part_major)
 
 
@@ -1258,7 +1258,7 @@
 text{*Existence of real and Standard Part Theorem*}
 lemma lemma_st_part_Ex:
      "(x::hypreal) \<in> HFinite
-       ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
+       ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
 apply (frule lemma_st_part_lub, safe)
 apply (frule isLubD1a)
 apply (blast dest: lemma_st_part_major2)
@@ -1483,13 +1483,13 @@
 apply (simp (no_asm) add: HInfinite_HFinite_iff)
 done
 
-lemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x"
+lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> @= x \<or> \<bar>x\<bar> @= -x"
 by (cut_tac x = x in hrabs_disj, auto)
 
 
 subsection{*Theorems about Monads*}
 
-lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x::hypreal) Un monad(-x)"
+lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)"
 by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
 
 lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
@@ -1505,7 +1505,7 @@
 apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
 done
 
-lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (abs x \<in> monad 0)"
+lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (\<bar>x\<bar> \<in> monad 0)"
 apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
 apply (auto simp add: monad_zero_minus_iff [symmetric])
 done
@@ -1543,7 +1543,7 @@
 done
 
 lemma Infinitesimal_approx_hrabs:
-     "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> abs x @= abs y"
+     "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
 apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
 apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
 done
@@ -1577,25 +1577,25 @@
      "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
 
-theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"
+theorem approx_hrabs: "(x::hypreal) @= y ==> \<bar>x\<bar> @= \<bar>y\<bar>"
 by (drule approx_hnorm, simp)
 
-lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"
+lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> @= 0 ==> x @= 0"
 apply (cut_tac x = x in hrabs_disj)
 apply (auto dest: approx_minus)
 done
 
 lemma approx_hrabs_add_Infinitesimal:
-  "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x+e)"
+  "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + e\<bar>"
 by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
 
 lemma approx_hrabs_add_minus_Infinitesimal:
-     "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x + -e)"
+     "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + -e\<bar>"
 by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
 
 lemma hrabs_add_Infinitesimal_cancel:
      "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
-         abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
+         \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
 apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
 apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
 apply (auto intro: approx_trans2)
@@ -1603,7 +1603,7 @@
 
 lemma hrabs_add_minus_Infinitesimal_cancel:
      "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
-         abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
+         \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
 apply (auto intro: approx_trans2)
@@ -1623,8 +1623,8 @@
 done
 
 lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
-     "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
-      ==> abs (hypreal_of_real r + x) < hypreal_of_real y"
+     "[| x \<in> Infinitesimal; \<bar>hypreal_of_real r\<bar> < hypreal_of_real y |]
+      ==> \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y"
 apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
 apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
 apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
@@ -1633,8 +1633,8 @@
 done
 
 lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
-     "[| x \<in> Infinitesimal;  abs(hypreal_of_real r) < hypreal_of_real y |]
-      ==> abs (x + hypreal_of_real r) < hypreal_of_real y"
+     "[| x \<in> Infinitesimal;  \<bar>hypreal_of_real r\<bar> < hypreal_of_real y |]
+      ==> \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y"
 apply (rule add.commute [THEN subst])
 apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
 done
@@ -1738,7 +1738,7 @@
 
 lemma monad_hrabs_less:
      "[| y \<in> monad x; 0 < hypreal_of_real e |]
-      ==> abs (y - x) < hypreal_of_real e"
+      ==> \<bar>y - x\<bar> < hypreal_of_real e"
 apply (drule mem_monad_approx [THEN approx_sym])
 apply (drule bex_Infinitesimal_iff [THEN iffD2])
 apply (auto dest!: InfinitesimalD)
@@ -1901,7 +1901,7 @@
 apply (rule st_le, auto)
 done
 
-lemma st_hrabs: "x \<in> HFinite ==> abs(st x) = st(abs x)"
+lemma st_hrabs: "x \<in> HFinite ==> \<bar>st x\<bar> = st \<bar>x\<bar>"
 apply (simp add: linorder_not_le st_zero_le abs_if st_minus
    linorder_not_less)
 apply (auto dest!: st_zero_ge [OF order_less_imp_le])
@@ -2077,12 +2077,12 @@
 lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
 by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
 
-lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}"
+lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. \<bar>real n\<bar> \<le> u}"
 apply (simp (no_asm) add: finite_real_of_nat_le_real)
 done
 
 lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
-     "\<not> eventually (\<lambda>n. abs(real n) \<le> u) FreeUltrafilterNat"
+     "\<not> eventually (\<lambda>n. \<bar>real n\<bar> \<le> u) FreeUltrafilterNat"
 by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
 
 lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
@@ -2092,8 +2092,8 @@
 done
 
 (*--------------------------------------------------------------
- The complement of {n. abs(real n) \<le> u} =
- {n. u < abs (real n)} is in FreeUltrafilterNat
+ The complement of {n. \<bar>real n\<bar> \<le> u} =
+ {n. u < \<bar>real n\<bar>} is in FreeUltrafilterNat
  by property of (free) ultrafilters
  --------------------------------------------------------------*)
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -228,8 +228,8 @@
 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
 
 lemma hcomplex_of_hypreal_abs:
-     "hcomplex_of_hypreal (abs x) =
-      hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
+     "hcomplex_of_hypreal \<bar>x\<bar> =
+      hcomplex_of_hypreal (hcmod (hcomplex_of_hypreal x))"
 by simp
 
 lemma HComplex_inject [simp]:
@@ -447,10 +447,10 @@
     "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
 by transfer simp
 
-lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
+lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = \<bar>y\<bar>"
 by transfer (simp add: norm_complex_def)
 
-lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
+lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = \<bar>y\<bar>"
 by transfer (simp add: norm_complex_def)
 
 (*---------------------------------------------------------------------------*)
@@ -506,11 +506,10 @@
 by transfer (simp add: cmod_unit_one)
 
 lemma hcmod_complex_polar [simp]:
-  "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
-      abs r"
+  "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \<bar>r\<bar>"
 by transfer (simp add: cmod_complex_polar)
 
-lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
+lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = \<bar>r\<bar>"
 by transfer (rule complex_mod_rcis)
 
 (*---------------------------------------------------------------------------*)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/NatStar.thy
--- a/src/HOL/NSA/NatStar.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/NatStar.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -96,7 +96,7 @@
 
 text{*Nonstandard extension with absolute value*}
 
-lemma starfun_abs: "!!N. ( *f* (%n. abs (f n))) N = abs(( *f* f) N)"
+lemma starfun_abs: "!!N. ( *f* (%n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
 by (transfer, rule refl)
 
 text{*The hyperpow function as a nonstandard extension of realpow*}
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/Star.thy
--- a/src/HOL/NSA/Star.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/Star.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -282,8 +282,7 @@
 text{*Alternative definition for hrabs with rabs function
    applied entrywise to equivalence class representative.
    This is easily proved using starfun and ns extension thm*}
-lemma hypreal_hrabs:
-     "abs (star_n X) = star_n (%n. abs (X n))"
+lemma hypreal_hrabs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
 by (simp only: starfun_rabs_hrabs [symmetric] starfun)
 
 text{*nonstandard extension of set through nonstandard extension
@@ -291,13 +290,12 @@
    where we replace rabs by some arbitrary function f and hrabs
    by its NS extenson. See second NS set extension below.*}
 lemma STAR_rabs_add_minus:
-   "*s* {x. abs (x + - y) < r} =
-     {x. abs(x + -star_of y) < star_of r}"
+   "*s* {x. \<bar>x + - y\<bar> < r} = {x. \<bar>x + -star_of y\<bar> < star_of r}"
 by (transfer, rule refl)
 
 lemma STAR_starfun_rabs_add_minus:
-  "*s* {x. abs (f x + - y) < r} =
-       {x. abs(( *f* f) x + -star_of y) < star_of r}"
+  "*s* {x. \<bar>f x + - y\<bar> < r} =
+       {x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}"
 by (transfer, rule refl)
 
 text{*Another characterization of Infinitesimal and one of @= relation.
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -583,7 +583,7 @@
 lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
 by (simp add: star_inverse_def)
 
-lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
+lemma Standard_abs: "x \<in> Standard \<Longrightarrow> \<bar>x\<bar> \<in> Standard"
 by (simp add: star_abs_def)
 
 lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
@@ -618,7 +618,7 @@
 lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
 by transfer (rule refl)
 
-lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
+lemma star_of_abs: "star_of \<bar>x\<bar> = \<bar>star_of x\<bar>"
 by transfer (rule refl)
 
 text {* @{term star_of} preserves numerals *}
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -53,7 +53,7 @@
 definition zcongm :: "int => int => int => bool"
   where "zcongm m = (\<lambda>a b. zcong a b m)"
 
-lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
+lemma abs_eq_1_iff [iff]: "(\<bar>z\<bar> = (1::int)) = (z = 1 \<or> z = -1)"
   -- \<open>LCP: not sure why this lemma is needed now\<close>
   by (auto simp add: abs_if)
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -566,7 +566,7 @@
 
 definition
   zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
-  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
+  "zgcd i j = int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>))"
 
 lemma zgcd_zdvd1 [iff, algebra]: "zgcd i j dvd i"
 by (simp add: zgcd_def int_dvd_iff)
@@ -611,7 +611,7 @@
     done
 qed
 
-lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
+lemma int_nat_abs: "int (nat \<bar>x\<bar>) = \<bar>x\<bar>" by arith
 
 lemma zgcd_greatest:
   assumes "k dvd m" and "k dvd n"
@@ -654,10 +654,10 @@
   with zgcd_pos show "?g' = 1" by simp
 qed
 
-lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
+lemma zgcd_0 [simp, algebra]: "zgcd m 0 = \<bar>m\<bar>"
   by (simp add: zgcd_def abs_if)
 
-lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
+lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = \<bar>m\<bar>"
   by (simp add: zgcd_def abs_if)
 
 lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
@@ -704,7 +704,7 @@
       add: minus_mult_right nat_mult_distrib zgcd_def abs_if
           mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult)
 
-lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
+lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = \<bar>k\<bar> * zgcd m n"
   by (simp add: abs_if zgcd_zmult_distrib2)
 
 lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
@@ -717,7 +717,7 @@
   by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
 
 
-definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
+definition "zlcm i j = int (lcm (nat \<bar>i\<bar>) (nat \<bar>j\<bar>))"
 
 lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
 by(simp add:zlcm_def dvd_int_iff)
@@ -729,7 +729,7 @@
 lemma dvd_imp_dvd_zlcm1:
   assumes "k dvd i" shows "k dvd (zlcm i j)"
 proof -
-  have "nat(abs k) dvd nat(abs i)" using \<open>k dvd i\<close>
+  have "nat \<bar>k\<bar> dvd nat \<bar>i\<bar>" using \<open>k dvd i\<close>
     by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
@@ -737,16 +737,16 @@
 lemma dvd_imp_dvd_zlcm2:
   assumes "k dvd j" shows "k dvd (zlcm i j)"
 proof -
-  have "nat(abs k) dvd nat(abs j)" using \<open>k dvd j\<close>
+  have "nat \<bar>k\<bar> dvd nat \<bar>j\<bar>" using \<open>k dvd j\<close>
     by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
 
 
-lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
+lemma zdvd_self_abs1: "(d::int) dvd \<bar>d\<bar>"
 by (case_tac "d <0", simp_all)
 
-lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
+lemma zdvd_self_abs2: "\<bar>d::int\<bar> dvd d"
 by (case_tac "d<0", simp_all)
 
 (* lcm a b is positive for positive a and b *)
@@ -776,8 +776,8 @@
   and bnz: "b \<noteq> 0" 
   shows "0 < zlcm a b"
 proof-
-  let ?na = "nat (abs a)"
-  let ?nb = "nat (abs b)"
+  let ?na = "nat \<bar>a\<bar>"
+  let ?nb = "nat \<bar>b\<bar>"
   have nap: "?na >0" using anz by simp
   have nbp: "?nb >0" using bnz by simp
   have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -2352,7 +2352,7 @@
 
 lemma integral_0_iff:
   fixes f :: "'a \<Rightarrow> real"
-  shows "integrable M f \<Longrightarrow> (\<integral>x. abs (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
+  shows "integrable M f \<Longrightarrow> (\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
   using integral_norm_eq_0_iff[of M f] by simp
 
 lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Probability/Interval_Integral.thy
--- a/src/HOL/Probability/Interval_Integral.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -1087,7 +1087,7 @@
 
 lemma interval_integral_norm2:
   "interval_lebesgue_integrable lborel a b f \<Longrightarrow> 
-    norm (LBINT t=a..b. f t) \<le> abs (LBINT t=a..b. norm (f t))"
+    norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
 proof (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -695,13 +695,13 @@
 
 lemma lborel_distr_mult':
   assumes "(c::real) \<noteq> 0"
-  shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. abs c)"
+  shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. \<bar>c\<bar>)"
 proof-
   have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
-  also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse (abs c) * abs c)" by (intro ext) simp
-  also have "density lborel ... = density (density lborel (\<lambda>_. inverse (abs c))) (\<lambda>_. abs c)"
+  also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
+  also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
     by (subst density_density_eq) auto
-  also from assms have "density lborel (\<lambda>_. inverse (abs c)) = distr lborel borel (op * c)"
+  also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (op * c)"
     by (rule lborel_distr_mult[symmetric])
   finally show ?thesis .
 qed
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Probability/Set_Integral.thy
--- a/src/HOL/Probability/Set_Integral.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Set_Integral.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -65,7 +65,7 @@
 *)
 
 (*
-lemma indicator_abs_eq: "\<And>A x. abs (indicator A x) = ((indicator A x) :: real)"
+lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
   by (auto simp add: indicator_def)
 *)
 
@@ -517,7 +517,7 @@
 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
 
 (*
-lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = abs a * cmod x"
+lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
   apply (simp add: norm_mult)
   by (subst norm_mult, auto)
 *)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -258,7 +258,7 @@
 lemma "(3 :: int) + 1 = 4" by smt
 lemma "x + (y + z) = y + (z + (x::int))" by smt
 lemma "max (3::int) 8 > 5" by smt
-lemma "abs (x :: real) + abs y \<ge> abs (x + y)" by smt
+lemma "\<bar>x :: real\<bar> + \<bar>y\<bar> \<ge> \<bar>x + y\<bar>" by smt
 lemma "P ((2::int) < 3) = P True" by smt
 lemma "x + 3 \<ge> 4 \<or> x < (1::int)" by smt
 
@@ -303,9 +303,9 @@
 processor.
 *}
 
-lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
-         x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
-         x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
+lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
+         x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
+         x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
  \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
   by smt
 
@@ -320,7 +320,7 @@
 
 lemma
   assumes "x \<noteq> (0::real)"
-  shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not> P then 4 else 2) * x"
+  shows "x + x \<noteq> (let P = (\<bar>x\<bar> > 1) in if P \<or> \<not> P then 4 else 2) * x"
   using assms [[z3_extensions]] by smt
 
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -336,11 +336,11 @@
   by smt+
 
 lemma
-  "abs (x::int) \<ge> 0"
-  "(abs x = 0) = (x = 0)"
-  "(x \<ge> 0) = (abs x = x)"
-  "(x \<le> 0) = (abs x = -x)"
-  "abs (abs x) = abs x"
+  "\<bar>x::int\<bar> \<ge> 0"
+  "(\<bar>x\<bar> = 0) = (x = 0)"
+  "(x \<ge> 0) = (\<bar>x\<bar> = x)"
+  "(x \<le> 0) = (\<bar>x\<bar> = -x)"
+  "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>"
   by smt+
 
 lemma
@@ -349,7 +349,7 @@
   "z < x \<and> z < y \<longrightarrow> z < min x y"
   "min x y = min y x"
   "x \<ge> 0 \<longrightarrow> min x 0 = 0"
-  "min x y \<le> abs (x + y)"
+  "min x y \<le> \<bar>x + y\<bar>"
   by smt+
 
 lemma
@@ -358,7 +358,7 @@
   "z > x \<and> z > y \<longrightarrow> z > max x y"
   "max x y = max y x"
   "x \<ge> 0 \<longrightarrow> max x 0 = x"
-  "max x y \<ge> - abs x - abs y"
+  "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>"
   by smt+
 
 lemma
@@ -448,11 +448,11 @@
   by smt+
 
 lemma
-  "abs (x::real) \<ge> 0"
-  "(abs x = 0) = (x = 0)"
-  "(x \<ge> 0) = (abs x = x)"
-  "(x \<le> 0) = (abs x = -x)"
-  "abs (abs x) = abs x"
+  "\<bar>x::real\<bar> \<ge> 0"
+  "(\<bar>x\<bar> = 0) = (x = 0)"
+  "(x \<ge> 0) = (\<bar>x\<bar> = x)"
+  "(x \<le> 0) = (\<bar>x\<bar> = -x)"
+  "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>"
   by smt+
 
 lemma
@@ -461,7 +461,7 @@
   "z < x \<and> z < y \<longrightarrow> z < min x y"
   "min x y = min y x"
   "x \<ge> 0 \<longrightarrow> min x 0 = 0"
-  "min x y \<le> abs (x + y)"
+  "min x y \<le> \<bar>x + y\<bar>"
   by smt+
 
 lemma
@@ -470,7 +470,7 @@
   "z > x \<and> z > y \<longrightarrow> z > max x y"
   "max x y = max y x"
   "x \<ge> 0 \<longrightarrow> max x 0 = x"
-  "max x y \<ge> - abs x - abs y"
+  "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>"
   by smt+
 
 lemma
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -172,7 +172,7 @@
 
 lemma bin_abs_lem:
   "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
-    nat (abs w) < nat (abs bin)"
+    nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
   apply clarsimp
   apply (unfold Bit_def)
   apply (cases b)
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -63,13 +63,13 @@
 lemma "(i::int) < j ==> min i j < max i j"
   by linarith
 
-lemma "(0::int) <= abs i"
+lemma "(0::int) <= \<bar>i\<bar>"
   by linarith
 
-lemma "(i::int) <= abs i"
+lemma "(i::int) <= \<bar>i\<bar>"
   by linarith
 
-lemma "abs (abs (i::int)) = abs i"
+lemma "\<bar>\<bar>i::int\<bar>\<bar> = \<bar>i\<bar>"
   by linarith
 
 text \<open>Also testing subgoals with bound variables.\<close>
@@ -127,7 +127,7 @@
 lemma "-(i::int) * 1 = 0 ==> i = 0"
   by linarith
 
-lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
+lemma "[| (0::int) < \<bar>i\<bar>; \<bar>i\<bar> * 1 < \<bar>i\<bar> * j |] ==> 1 < \<bar>i\<bar> * j"
   by linarith
 
 
@@ -227,13 +227,13 @@
 text \<open>Splitting of inequalities of different type.\<close>
 
 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
-  a + b <= nat (max (abs i) (abs j))"
+  a + b <= nat (max \<bar>i\<bar> \<bar>j\<bar>)"
   by linarith
 
 text \<open>Again, but different order.\<close>
 
 lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
-  a + b <= nat (max (abs i) (abs j))"
+  a + b <= nat (max \<bar>i\<bar> \<bar>j\<bar>)"
   by linarith
 
 end
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -1231,7 +1231,7 @@
   real_less_def: "x < (y::real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
 
 definition
-  real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
+  real_abs_def: "\<bar>r::real\<bar> = (if r < 0 then - r else r)"
 
 definition
   real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/ex/Normalization_by_Evaluation.thy
--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -92,14 +92,14 @@
 
 lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
 lemma "(-4::int) * 2 = -8" by normalization
-lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
+lemma "\<bar>(-4::int) + 2 * 1\<bar> = 2" by normalization
 lemma "(2::int) + 3 = 5" by normalization
 lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
 lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
 lemma "(2::int) < 3" by normalization
 lemma "(2::int) <= 3" by normalization
-lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
-lemma "4 - 42 * abs (3 + (-7::int)) = -164" by normalization
+lemma "\<bar>(-4::int) + 2 * 1\<bar> = 2" by normalization
+lemma "4 - 42 * \<bar>3 + (-7::int)\<bar> = -164" by normalization
 lemma "(if (0::nat) \<le> (x::nat) then 0::nat else x) = 0" by normalization
 lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
 lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/ex/PresburgerEx.thy
--- a/src/HOL/ex/PresburgerEx.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/PresburgerEx.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -100,9 +100,9 @@
 
 Warning: it takes (in 2006) over 4.2 minutes!\<close>
 
-lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
-         x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
-         x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
+lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
+         x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
+         x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
  \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
 by arith
 
diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/ex/Set_Theory.thy
--- a/src/HOL/ex/Set_Theory.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Set_Theory.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -193,8 +193,8 @@
   \<comment> \<open>Example 7.\<close>
   by force
 
-lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
-    \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. abs y \<notin> A))"
+lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> \<bar>v\<bar>)
+    \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. \<bar>y\<bar> \<notin> A))"
   \<comment> \<open>Example 8 needs a small hint.\<close>
   by force
     \<comment> \<open>not \<open>blast\<close>, which can't simplify \<open>-2 < 0\<close>\<close>