src/HOL/Fields.thy

--- a/src/HOL/Fields.thy	Wed Jul 08 14:01:41 2015 +0200
+++ b/src/HOL/Fields.thy	Wed Jul 08 20:19:12 2015 +0200
@@ -145,9 +145,6 @@
 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
 by (simp add: divide_inverse algebra_simps)
 
-lemma divide_1 [simp]: "a / 1 = a"
-  by (simp add: divide_inverse)
-
 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   by (simp add: divide_inverse mult.assoc)