src/HOL/Algebra/FiniteProduct.thy
changeset 32693 6c6b1ba5e71e
parent 31727 2621a957d417
child 32960 69916a850301
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 21 15:35:14 2009 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 21 15:35:15 2009 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4    apply (induct set: finite)
     1.5     apply simp
     1.6    apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
     1.7 -    Int_mono2 Un_subset_iff)
     1.8 +    Int_mono2)
     1.9    done
    1.10  
    1.11  lemma (in LCD) foldD_nest_Un_disjoint:
    1.12 @@ -274,14 +274,14 @@
    1.13    apply (simp add: AC insert_absorb Int_insert_left
    1.14      LCD.foldD_insert [OF LCD.intro [of D]]
    1.15      LCD.foldD_closed [OF LCD.intro [of D]]
    1.16 -    Int_mono2 Un_subset_iff)
    1.17 +    Int_mono2)
    1.18    done
    1.19  
    1.20  lemma (in ACeD) foldD_Un_disjoint:
    1.21    "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
    1.22      foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
    1.23    by (simp add: foldD_Un_Int
    1.24 -    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
    1.25 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]])
    1.26  
    1.27  
    1.28  subsubsection {* Products over Finite Sets *}
    1.29 @@ -377,7 +377,7 @@
    1.30    from insert have A: "g \<in> A -> carrier G" by fast
    1.31    from insert A a show ?case
    1.32      by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
    1.33 -          Int_mono2 Un_subset_iff) 
    1.34 +          Int_mono2) 
    1.35  qed
    1.36  
    1.37  lemma finprod_Un_disjoint: