--- a/src/HOL/Fields.thy Tue Apr 27 12:20:09 2010 +0200
+++ b/src/HOL/Fields.thy Tue Apr 27 12:20:17 2010 +0200
@@ -811,7 +811,6 @@
apply (auto simp add: mult_commute)
done
-
text{*Simplify quotients that are compared with the value 1.*}
lemma le_divide_eq_1 [no_atp]: