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/Starlike.thy
changeset 68796 9ca183045102
parent 68607 67bb59e49834
child 69064 5840724b1d71 
--- a/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:37 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:39 2018 +0000
@@ -1355,7 +1355,7 @@
     proof safe
       fix i :: 'a
       assume i: "i \<in> Basis"
-      have "norm (x - y) < MINIMUM Basis ((\<bullet>) x)"
+      have "norm (x - y) < Min (((\<bullet>) x) ` Basis)"
         using y by (auto simp: dist_norm less_eq_real_def)
       also have "... \<le> x\<bullet>i"
         using i by auto
isabelle