src/HOL/Library/Determinants.thy
changeset 30837 3d4832d9f7e4
parent 30661 54858c8ad226
child 30843 3419ca741dbf
     1.1 --- a/src/HOL/Library/Determinants.thy	Tue Mar 31 15:57:10 2009 -0700
     1.2 +++ b/src/HOL/Library/Determinants.thy	Wed Apr 01 16:03:00 2009 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4    moreover
     1.5    {assume fS: "finite S"
     1.6      then have ?thesis
     1.7 -      apply (simp add: setprod_def)
     1.8 +      apply (simp add: setprod_def cong del:strong_setprod_cong)
     1.9        apply (rule ab_semigroup_mult.fold_image_permute)
    1.10        apply (auto simp add: p)
    1.11        apply unfold_locales
    1.12 @@ -115,7 +115,7 @@
    1.13  qed
    1.14  
    1.15  lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
    1.16 -  by (auto intro: setprod_permute)
    1.17 +  by (blast intro!: setprod_permute)
    1.18  
    1.19  (* ------------------------------------------------------------------------- *)
    1.20  (* Basic determinant properties.                                             *)