src/HOL/Archimedean_Field.thy
changeset 54281 b01057e72233
parent 47592 a6b76247534d
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Archimedean_Field.thy	Wed Nov 06 14:50:50 2013 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Nov 05 21:23:42 2013 +0100
     1.3 @@ -129,12 +129,8 @@
     1.4    fix y z assume
     1.5      "of_int y \<le> x \<and> x < of_int (y + 1)"
     1.6      "of_int z \<le> x \<and> x < of_int (z + 1)"
     1.7 -  then have
     1.8 -    "of_int y \<le> x" "x < of_int (y + 1)"
     1.9 -    "of_int z \<le> x" "x < of_int (z + 1)"
    1.10 -    by simp_all
    1.11 -  from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`]
    1.12 -       le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`]
    1.13 +  with le_less_trans [of "of_int y" "x" "of_int (z + 1)"]
    1.14 +       le_less_trans [of "of_int z" "x" "of_int (y + 1)"]
    1.15    show "y = z" by (simp del: of_int_add)
    1.16  qed
    1.17