equal
deleted
inserted
replaced
171 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
171 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
172 val conj_comms = [conj_commute, conj_left_commute]; |
172 val conj_comms = [conj_commute, conj_left_commute]; |
173 |
173 |
174 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
174 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
175 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
175 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
|
176 |
|
177 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; |
|
178 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; |
|
179 |