src/HOL/Archimedean_Field.thy
changeset 61738 c4f6031f1310
parent 61649 268d88ec9087
child 61942 f02b26f7d39d
     1.1 --- a/src/HOL/Archimedean_Field.thy	Sun Nov 22 23:19:43 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Nov 23 16:57:54 2015 +0000
     1.3 @@ -657,7 +657,7 @@
     1.4  proof (cases "of_int m \<ge> z")
     1.5    case True
     1.6    hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
     1.7 -    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
     1.8 +    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
     1.9    also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
    1.10    with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
    1.11      by (simp add: ceiling_le_iff)
    1.12 @@ -665,7 +665,7 @@
    1.13  next
    1.14    case False
    1.15    hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
    1.16 -    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
    1.17 +    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith?
    1.18    also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
    1.19    with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
    1.20      by (simp add: le_floor_iff)