# HG changeset patch
# User paulson
# Date 950884529 -3600
# Node ID 38f96394c099af1226208077419a4e0e00008c80
# Parent  84a5fe44520faf122bfb9ceff53b84a6507a97d0
new distributive laws

diff -r 84a5fe44520f -r 38f96394c099 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Feb 18 15:34:22 2000 +0100
+++ b/src/HOL/Prod.ML	Fri Feb 18 15:35:29 2000 +0100
@@ -466,6 +466,19 @@
 by (Blast_tac 1);
 qed "Sigma_Union";
 
+(*Non-dependent versions are needed to avoid the need for higher-order
+  matching, especially when the rules are re-oriented*)
+Goal "(A Un B) Times C = (A Times C) Un (B Times C)";
+by (Blast_tac 1);
+qed "Times_Un_distrib1"; 
+
+Goal "(A Int B) Times C = (A Times C) Int (B Times C)";
+by (Blast_tac 1);
+qed "Times_Int_distrib1"; 
+
+Goal "(A - B) Times C = (A Times C) - (B Times C)";
+by (Blast_tac 1);
+qed "Times_Diff_distrib1"; 
 
 (** Exhaustion rule for unit -- a degenerate form of induction **)