src/HOL/simpdata.ML
changeset 1892 23765bc3e8e2
parent 1874 35f22792aade
child 1922 ce495557ac33
     1.1 --- a/src/HOL/simpdata.ML	Fri Jul 26 12:31:04 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Jul 29 18:30:01 1996 +0200
     1.3 @@ -185,6 +185,12 @@
     1.4  prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
     1.5  prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";
     1.6  
     1.7 +prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))";
     1.8 +prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))";
     1.9 +
    1.10 +prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))";
    1.11 +prove "imp_conj_assoc"   "((P&Q)-->R)   = (P --> (Q --> R))";
    1.12 +
    1.13  prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
    1.14  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
    1.15