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/Limits.thy
changeset 70817 dd675800469d
parent 70804 4eef7c6ef7bf
child 70999 5b753486c075 
--- a/src/HOL/Limits.thy	Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/Limits.thy	Wed Oct 09 14:51:54 2019 +0000
@@ -285,7 +285,7 @@
   with Bfun_const have "Bseq (\<lambda>x. inverse c * (c * f x))"
     by (rule Bseq_mult)
   with \<open>c \<noteq> 0\<close> show "Bseq f"
-    by (simp add: divide_simps)
+    by (simp add: field_split_simps)
 qed (intro Bseq_mult Bfun_const)
 
 lemma Bseq_subseq: "Bseq f \<Longrightarrow> Bseq (\<lambda>x. f (g x))"
isabelle