src/HOL/Archimedean_Field.thy

--- a/src/HOL/Archimedean_Field.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -395,9 +395,9 @@
       by blast
     then have l: "l = - r"
       by simp
-    moreover with \<open>l \<noteq> 0\<close> False have "r > 0"
+    with \<open>l \<noteq> 0\<close> False have "r > 0"
       by simp
-    ultimately show ?thesis
+    with l show ?thesis
       using pos_mod_bound [of r]
       by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
   qed