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: