# HG changeset patch
# User paulson
# Date 877008233 -7200
# Node ID c0d56e4c823e0acad97d268df58d6fa886e86083
# Parent  1b29151a100995157d42583715fcb49e70da0015
New simprules imp_disj1, imp_disj2

diff -r 1b29151a1009 -r c0d56e4c823e src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Oct 16 15:23:25 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Oct 16 15:23:53 1997 +0200
@@ -238,6 +238,9 @@
 prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
 prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
 
+prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
+prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";
+
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
 prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
@@ -371,7 +374,7 @@
        True_implies_equals, (* prune asms `True' *)
        if_True, if_False, if_cancel,
        o_apply, imp_disjL, conj_assoc, disj_assoc,
-       de_Morgan_conj, de_Morgan_disj, not_imp,
+       de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
        not_all, not_ex, cases_simp]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defEX_regroup]