src/HOL/Decision_Procs/Approximation_Bounds.thy
changeset 70347 e5cd5471c18a
parent 70097 4005298550a6
child 70350 571ae57313a4
     1.1 --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -1588,7 +1588,7 @@
     1.4      by (cases "k = 0")
     1.5        (auto intro!: add_mono
     1.6          simp add: k [symmetric] uminus_add_conv_diff [symmetric]
     1.7 -        simp del: float_of_numeral uminus_add_conv_diff)
     1.8 +        simp del: uminus_add_conv_diff)
     1.9    hence "?lx \<le> x - k * (2 * pi) \<and> x - k * (2 * pi) \<le> ?ux"
    1.10      by (auto intro!: float_plus_down_le float_plus_up_le)
    1.11    note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]