changeset 78497 | b159a5496a3e |
parent 78099 | 4d9349989d94 |
child 78794 | c74fd21af246 |
--- 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"