Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Wed, 09 Aug 2023 14:33:59 +0200
changeset 78498 964de51dd2e4
parent 78496 2a26d423d9fb (current diff)
parent 78497 b159a5496a3e (diff)
child 78499 a7dab3b8ebfe
merged
--- 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"
isabelle