src/HOL/simpdata.ML
changeset 3904 c0d56e4c823e
parent 3896 ee8ebb74ec00
child 3913 96e28b16861c
     1.1 --- a/src/HOL/simpdata.ML	Thu Oct 16 15:23:25 1997 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Oct 16 15:23:53 1997 +0200
     1.3 @@ -238,6 +238,9 @@
     1.4  prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
     1.5  prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
     1.6  
     1.7 +prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
     1.8 +prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";
     1.9 +
    1.10  prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
    1.11  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
    1.12  prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
    1.13 @@ -371,7 +374,7 @@
    1.14         True_implies_equals, (* prune asms `True' *)
    1.15         if_True, if_False, if_cancel,
    1.16         o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.17 -       de_Morgan_conj, de_Morgan_disj, not_imp,
    1.18 +       de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
    1.19         not_all, not_ex, cases_simp]
    1.20       @ ex_simps @ all_simps @ simp_thms)
    1.21       addsimprocs [defEX_regroup]