src/HOL/Library/Determinants.thy
changeset 30843 3419ca741dbf
parent 30837 3d4832d9f7e4
child 31280 8ef7ba78bf26
     1.1 --- a/src/HOL/Library/Determinants.thy	Wed Apr 01 18:41:15 2009 +0200
     1.2 +++ b/src/HOL/Library/Determinants.thy	Wed Apr 01 22:29:10 2009 +0200
     1.3 @@ -310,10 +310,7 @@
     1.4  using r
     1.5  apply (simp add: row_def det_def Cart_eq)
     1.6  apply (rule setsum_0')
     1.7 -apply (clarsimp simp add: sign_nz)
     1.8 -apply (rule setprod_zero)
     1.9 -apply simp
    1.10 -apply auto
    1.11 +apply (auto simp: sign_nz)
    1.12  done
    1.13  
    1.14  lemma det_zero_column: