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")
```