src/HOL/simpdata.ML

 
 (*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 "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)";
 prove "not_iff" "(P~=Q) = (P = (~Q))";
 

     HOL_basic_ss addsimps 
      ([triv_forall_equality, (* prunes params *)
        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]
      addcongs [imp_cong];