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