| changeset 60570 | 7ed2cde6806d |
| parent 60353 | 838025c6e278 |
| child 60690 | a9e45c9588c3 |
--- a/src/HOL/Fields.thy Thu Jun 25 15:01:41 2015 +0200 +++ b/src/HOL/Fields.thy Thu Jun 25 15:01:42 2015 +0200 @@ -139,9 +139,6 @@ lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" by (simp add: divide_inverse) -lemma divide_zero_left [simp]: "0 / a = 0" -by (simp add: divide_inverse) - lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a" by (simp add: divide_inverse)