# HG changeset patch
# User nipkow
# Date 1691565735 -7200
# Node ID b159a5496a3e9c15289993ac69d47521249bf2d1
# Parent  10264fe8012f3825418f434afb025b9888a422be
improved simp rule insert_Times_insert (following Dominique Unruh).

diff -r 10264fe8012f -r b159a5496a3e src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 09 08:24:24 2023 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 09 09:22:15 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"