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/Hahn_Banach/Function_Norm.thy
changeset 57512 cc97b347b301
parent 50918 3b6417e9f73e
child 58744 c434e37f290e 
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -141,7 +141,7 @@
             then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
           qed
           also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
-            by (rule Groups.mult_assoc)
+            by (rule Groups.mult.assoc)
           also
           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
           then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
isabelle