# HG changeset patch
# User chaieb
# Date 1236194488 0
# Node ID 11cb411913b4dfd81df6bdbefdc88933e4d6cae3
# Parent  478e5348ad3cad784e91bf9ed27aff8e37ef02cb
fixed proofs

diff -r 478e5348ad3c -r 11cb411913b4 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy	Wed Mar 04 10:54:47 2009 +0000
+++ b/src/HOL/Library/Determinants.thy	Wed Mar 04 19:21:28 2009 +0000
@@ -176,7 +176,7 @@
     from ld[OF i(1) piU i(2)] i(1) have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
     from setprod_zero[OF fU ex] have "?pp p = 0" by simp}
   then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"  by blast
-  from setsum_superset[OF fPU id0 p0] show ?thesis
+  from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
     unfolding det_def by (simp add: sign_id)
 qed
 
@@ -199,7 +199,7 @@
     from ld[OF i(1) piU i(2)] i(1) have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
     from setprod_zero[OF fU ex] have "?pp p = 0" by simp}
   then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"  by blast
-  from setsum_superset[OF fPU id0 p0] show ?thesis
+  from   setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
     unfolding det_def by (simp add: sign_id)
 qed
 
@@ -750,8 +750,8 @@
   have "det (A**B) = setsum (\<lambda>f.  det (\<chi> i. A $ i $ f i *s B $ f i)) ?F"
     unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] .. 
   also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU"
-    unfolding setsum_superset[OF fF PUF zth, symmetric] 
-    unfolding det_rows_mul ..
+    using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric] 
+    unfolding det_rows_mul by auto
   finally show ?thesis unfolding th2 .
 qed