# HG changeset patch
# User huffman
# Date 1313020923 25200
# Node ID 0697c01ff3ea0edc2a503705ed7a8a47b6231dc7
# Parent  2c10c35dd4bec36a75614a855e1999b4b8d74daa
follow standard naming scheme for sgn_vec_def

diff -r 2c10c35dd4be -r 0697c01ff3ea src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 16:35:50 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 17:02:03 2011 -0700
@@ -373,8 +373,7 @@
 
 definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
 
-definition vector_sgn_def:
-  "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
+definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
 
 instance proof
   fix a :: real and x y :: "'a ^ 'b"
@@ -393,7 +392,7 @@
     unfolding norm_vec_def
     by (simp add: setL2_right_distrib)
   show "sgn x = scaleR (inverse (norm x)) x"
-    by (rule vector_sgn_def)
+    by (rule sgn_vec_def)
   show "dist x y = norm (x - y)"
     unfolding dist_vec_def norm_vec_def
     by (simp add: dist_norm)