# HG changeset patch
# User paulson
# Date 866712211 -7200
# Node ID 8a79e27ac53b039f28f2f978fd1283bcbc421e8c
# Parent  c7c8c0db05b98fe4af6afcd4d25e9b8cca9798bb
Two new rewrite rules--NOT included by default\!

diff -r c7c8c0db05b9 -r 8a79e27ac53b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Jun 18 15:38:35 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Jun 19 11:23:31 1997 +0200
@@ -175,6 +175,10 @@
 prove "imp_conjL" "((P&Q) -->R)  = (P --> (Q --> R))";
 prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
 
+(*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
+prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
+prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
+
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
 prove "not_imp" "(~(P --> Q)) = (P & ~Q)";