src/HOL/ex/Arith_Examples.thy

   by linarith
 
 lemma "(i::int) < j ==> min i j < max i j"
   by linarith
 
-lemma "(0::int) <= abs i"
-  by linarith
-
-lemma "(i::int) <= abs i"
-  by linarith
-
-lemma "abs (abs (i::int)) = abs i"
+lemma "(0::int) <= \<bar>i\<bar>"
+  by linarith
+
+lemma "(i::int) <= \<bar>i\<bar>"
+  by linarith
+
+lemma "\<bar>\<bar>i::int\<bar>\<bar> = \<bar>i\<bar>"
   by linarith
 
 text \<open>Also testing subgoals with bound variables.\<close>
 
 lemma "!!x. (x::nat) <= y ==> x - y = 0"

   by linarith
 
 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
 
 
 subsection \<open>Meta-Logic\<close>
 

   by linarith
 
 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