# HG changeset patch
# User nipkow
# Date 1691584439 -7200
# Node ID 964de51dd2e4780b475ccae70a4afc2460728868
# Parent  2a26d423d9fb9e79b1e84621fbeeace6c43dd205# Parent  b159a5496a3e9c15289993ac69d47521249bf2d1
merged

diff -r 2a26d423d9fb -r 964de51dd2e4 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 09 11:04:17 2023 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 09 14:33:59 2023 +0200
@@ -1159,7 +1159,7 @@
   by auto
 
 lemma insert_Times_insert [simp]:
-  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
+  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> {a} \<times> B)"
   by blast
 
 lemma vimage_Times: "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"