src/HOL/Groups_Big.thy
changeset 61032 b57df8eecad6
parent 60974 6a6f15d8fbc4
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Groups_Big.thy	Thu Aug 27 13:07:45 2015 +0200
     1.2 +++ b/src/HOL/Groups_Big.thy	Thu Aug 27 21:19:48 2015 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4    using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
     1.5  
     1.6  lemma Sigma:
     1.7 -  "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
     1.8 +  "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
     1.9  apply (subst Sigma_def)
    1.10  apply (subst UNION_disjoint, assumption, simp)
    1.11   apply blast
    1.12 @@ -350,7 +350,7 @@
    1.13  qed
    1.14  
    1.15  lemma cartesian_product:
    1.16 -   "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
    1.17 +   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
    1.18  apply (rule sym)
    1.19  apply (cases "finite A") 
    1.20   apply (cases "finite B")