# HG changeset patch
# User huffman
# Date 1243556658 25200
# Node ID a2f737a726552ad9342432182f6f503f2db9ada5
# Parent  f41c023d90bc5e2c67d89800d4c26c6facbe1ba1
fix references to dist_def

diff -r f41c023d90bc -r a2f737a72655 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy	Thu May 28 17:09:51 2009 -0700
+++ b/src/HOL/Library/Determinants.thy	Thu May 28 17:24:18 2009 -0700
@@ -923,10 +923,10 @@
   shows "linear f"
 proof-
   {fix v w
-    {fix x note fd[rule_format, of x 0, unfolded dist_def f0 diff_0_right] }
+    {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }
     note th0 = this
     have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
-      unfolding dot_norm_neg dist_def[symmetric]
+      unfolding dot_norm_neg dist_norm[symmetric]
       unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
   note fc = this
   show ?thesis unfolding linear_def vector_eq
@@ -947,7 +947,7 @@
   unfolding orthogonal_transformation
   apply (rule iffI)
   apply clarify
-  apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_def)
+  apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm)
   apply (rule conjI)
   apply (rule isometry_linear)
   apply simp
@@ -955,7 +955,7 @@
   apply clarify
   apply (erule_tac x=v in allE)
   apply (erule_tac x=0 in allE)
-  by (simp add: dist_def)
+  by (simp add: dist_norm)
 
 (* ------------------------------------------------------------------------- *)
 (* Can extend an isometry from unit sphere.                                  *)
@@ -995,13 +995,13 @@
     moreover
     {assume "x = 0" "y \<noteq> 0"
       then have "dist (?g x) (?g y) = dist x y"
-	apply (simp add: dist_def norm_mul)
+	apply (simp add: dist_norm norm_mul)
 	apply (rule f1[rule_format])
 	by(simp add: norm_mul field_simps)}
     moreover
     {assume "x \<noteq> 0" "y = 0"
       then have "dist (?g x) (?g y) = dist x y"
-	apply (simp add: dist_def norm_mul)
+	apply (simp add: dist_norm norm_mul)
 	apply (rule f1[rule_format])
 	by(simp add: norm_mul field_simps)}
     moreover
@@ -1015,9 +1015,9 @@
 	"norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
 	norm (inverse (norm x) *s x - inverse (norm y) *s y)"
 	using z
-	by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
+	by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
       from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
-	by (simp add: dist_def)}
+	by (simp add: dist_norm)}
     ultimately have "dist (?g x) (?g y) = dist x y" by blast}
   note thd = this
     show ?thesis