changeset 69939 | 812ce526da33 |
parent 69922 | 4a9167f377b0 |
child 69994 | cf7150ab1075 |
--- a/src/HOL/Product_Type.thy Wed Mar 20 23:06:51 2019 +0100 +++ b/src/HOL/Product_Type.thy Thu Mar 21 14:18:22 2019 +0000 @@ -1134,7 +1134,7 @@ by (cases "f x") (auto split: prod.split) qed -lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" +lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" by auto lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"