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/Analysis/Conformal_Mappings.thy
changeset 70113 c8deb8ba6d05
parent 70065 cc89a395b5a3
child 70136 f03a01a18c6e 
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -1070,7 +1070,7 @@
   proof (cases "\<forall>i\<le>n. 0<i \<longrightarrow> a i = 0")
     case True
     then have [simp]: "\<And>z. f z = a 0"
-      by (simp add: that sum_atMost_shift)
+      by (simp add: that sum.atMost_shift)
     have False using compf [of "{a 0}"] by simp
     then show ?thesis ..
   next
isabelle