# HG changeset patch # User nipkow # Date 1225968762 -3600 # Node ID 01e04e41cc7b0fa6136cb4f4f43e464a9ccb14ed # Parent ef16499edaab201b0ec06d3ca7ca0d3a8e01e76a added lemma diff -r ef16499edaab -r 01e04e41cc7b src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Nov 06 10:05:48 2008 +0100 +++ b/src/HOL/Product_Type.thy Thu Nov 06 11:52:42 2008 +0100 @@ -904,14 +904,18 @@ *} lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" - by blast +by blast lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" - by blast +by blast lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" - by blast +by blast +lemma insert_times_insert[simp]: + "insert a A \ insert b B = + insert (a,b) (A \ insert b B \ insert a A \ B)" +by blast subsubsection {* Code generator setup *}