src/HOL/Product_Type.thy
changeset 28719 01e04e41cc7b
parent 28562 4e74209f113e
child 30604 2a9911f4b0a3
     1.1 --- a/src/HOL/Product_Type.thy	Thu Nov 06 10:05:48 2008 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Nov 06 11:52:42 2008 +0100
     1.3 @@ -904,14 +904,18 @@
     1.4  *}
     1.5  
     1.6  lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
     1.7 -  by blast
     1.8 +by blast
     1.9  
    1.10  lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
    1.11 -  by blast
    1.12 +by blast
    1.13  
    1.14  lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
    1.15 -  by blast
    1.16 +by blast
    1.17  
    1.18 +lemma insert_times_insert[simp]:
    1.19 +  "insert a A \<times> insert b B =
    1.20 +   insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
    1.21 +by blast
    1.22  
    1.23  subsubsection {* Code generator setup *}
    1.24