# HG changeset patch
# User paulson
# Date 838657801 -7200
# Node ID 23765bc3e8e27980a8243e35be4f28f172add54b
# Parent  618f48bd45325c557b6accd6becf0a08d17629fa
Added two new distributive laws

diff -r 618f48bd4532 -r 23765bc3e8e2 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Jul 26 12:31:04 1996 +0200
+++ b/src/HOL/simpdata.ML	Mon Jul 29 18:30:01 1996 +0200
@@ -185,6 +185,12 @@
 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";
 
+prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))";
+prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))";
+
+prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))";
+prove "imp_conj_assoc"   "((P&Q)-->R)   = (P --> (Q --> R))";
+
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";