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/Library/Euclidean_Space.thy
changeset 31587 a7e187205fc0
parent 31568 963caf6fa234
child 31590 776d6a4c1327 
--- a/src/HOL/Library/Euclidean_Space.thy	Fri Jun 12 11:39:23 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Fri Jun 12 12:00:30 2009 -0700
@@ -771,7 +771,7 @@
     done
   show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
     unfolding vector_norm_def
-    by (simp add: norm_scaleR setL2_right_distrib)
+    by (simp add: setL2_right_distrib)
   show "sgn x = scaleR (inverse (norm x)) x"
     by (rule vector_sgn_def)
   show "dist x y = norm (x - y)"
isabelle