src/HOL/SetInterval.thy
changeset 23398 0b5a400c7595
parent 23277 aa158e145ea3
child 23413 5caa2710dd5b
     1.1 --- a/src/HOL/SetInterval.thy	Fri Jun 15 09:10:06 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Jun 15 15:10:32 2007 +0200
     1.3 @@ -742,7 +742,7 @@
     1.4    apply (induct "n", auto)
     1.5    apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
     1.6    apply (auto simp add: mult_assoc left_distrib)
     1.7 -  apply (simp add: times_divide_eq_right [symmetric] divide_self)
     1.8 +  apply (simp add: times_divide_eq_right [symmetric])
     1.9    apply (simp add: right_distrib diff_minus mult_commute power_Suc)
    1.10    done
    1.11