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