| changeset 36365 | 18bf20d0c2df |
| parent 36364 | 0e2679025aeb |
| parent 36350 | bc7982c54e37 |
| child 36755 | d1b498f2f50b |
--- a/src/HOL/SetInterval.thy Mon Apr 26 09:37:46 2010 -0700 +++ b/src/HOL/SetInterval.thy Mon Apr 26 09:45:22 2010 -0700 @@ -1095,7 +1095,7 @@ next case (Suc n) moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp - ultimately show ?case by (simp add: field_eq_simps divide_inverse) + ultimately show ?case by (simp add: field_simps divide_inverse) qed ultimately show ?thesis by simp qed