src/HOL/Product_Type.thy
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"