src/HOL/Library/Groups_Big_Fun.thy
changeset 61424 c3658c18b7bc
parent 61378 3e04c9ca001a
child 61605 1bf7b186542e
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4    have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
     1.5      by (auto intro!: bijI injI simp add: image_def)
     1.6    have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
     1.7 -    by auto (insert subset, auto)
     1.8 +    by auto (insert subset, blast)
     1.9    with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
    1.10      by (rule cartesian_product)
    1.11    then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"