Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SetInterval.thy
changeset 23398 0b5a400c7595
parent 23277 aa158e145ea3
child 23413 5caa2710dd5b 
--- a/src/HOL/SetInterval.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/SetInterval.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -742,7 +742,7 @@
   apply (induct "n", auto)
   apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
   apply (auto simp add: mult_assoc left_distrib)
-  apply (simp add: times_divide_eq_right [symmetric] divide_self)
+  apply (simp add: times_divide_eq_right [symmetric])
   apply (simp add: right_distrib diff_minus mult_commute power_Suc)
   done
isabelle