| changeset 56077 | d397030fb27e |
| parent 55932 | 68c5104d2204 |
| child 56218 | 1c3f1f2431f9 |
--- a/src/HOL/Product_Type.thy Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Product_Type.thy Thu Mar 13 08:56:08 2014 +0100 @@ -1125,7 +1125,7 @@ lemma swap_product: "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A" - by (simp add: split_def image_def) blast + by (simp add: split_def image_def set_eq_iff) lemma image_split_eq_Sigma: "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"