# HG changeset patch
# User himmelma
# Date 1243518860 -7200
# Node ID 8ef7ba78bf260e5cf4d44cedb276412a456e24a8
# Parent  4ae81233cf69c57ddd89584a4347f8c0deeeaad7
corrected problem in Determinants

diff -r 4ae81233cf69 -r 8ef7ba78bf26 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy	Thu May 28 15:42:44 2009 +0200
+++ b/src/HOL/Library/Determinants.thy	Thu May 28 15:54:20 2009 +0200
@@ -733,7 +733,7 @@
       apply simp
       done
     from c ci
-    have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s c j *s row j A) (?U - {i})"
+    have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
       unfolding setsum_diff1'[OF fU iU] setsum_cmul
       apply -
       apply (rule vector_mul_lcancel_imp[OF ci])
@@ -1006,7 +1006,7 @@
 	by(simp add: norm_mul field_simps)}
     moreover
     {assume z: "x \<noteq> 0" "y \<noteq> 0"
-      have th00: "x = norm x *s inverse (norm x) *s x" "y = norm y *s inverse (norm y) *s y" "norm x *s f (inverse (norm x) *s x) = norm x *s f (inverse (norm x) *s x)"
+      have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)"
 	"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"
 	"norm (inverse (norm x) *s x) = 1"
 	"norm (f (inverse (norm x) *s x)) = 1"