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)