src/HOL/Decision_Procs/Approximation.thy
changeset 44821 a92f65e174cf
parent 44568 e6f291cb5810
child 45129 1fce03e3e8ad
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -295,7 +295,7 @@
     1.4          unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
     1.5        also have "\<dots> < pow2 (?E div 2) * 2"
     1.6          by (rule mult_strict_left_mono, auto intro: E_mod_pow)
     1.7 -      also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
     1.8 +      also have "\<dots> = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto
     1.9        finally show ?thesis by auto
    1.10      qed
    1.11      finally show ?thesis