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/Multivariate_Analysis/Cauchy_Integral_Thm.thy
changeset 62101 26c0a70f78a3
parent 62087 44841d07ef1d
child 62131 1baed43f453e 
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -4106,7 +4106,7 @@
       done
   } then
   show ?thesis
-    by (auto simp: Complex.open_complex_def)
+    by (auto simp: open_dist)
 qed
 
 subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
isabelle