src/HOL/simpdata.ML
changeset 4743 b3bfcbd9fb93
parent 4718 fc2ba9fb2135
child 4744 4469d498cd48
     1.1 --- a/src/HOL/simpdata.ML	Thu Mar 12 13:15:36 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Mar 12 13:17:13 1998 +0100
     1.3 @@ -208,8 +208,8 @@
     1.4  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
     1.5  prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
     1.6  prove "not_iff" "(P~=Q) = (P = (~Q))";
     1.7 -prove "not1_or" "(~P | Q) = (P --> Q)";
     1.8 -prove "not2_or" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
     1.9 +prove "disj_not1" "(~P | Q) = (P --> Q)";
    1.10 +prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
    1.11  
    1.12  (*Avoids duplication of subgoals after expand_if, when the true and false 
    1.13    cases boil down to the same thing.*) 
    1.14 @@ -410,7 +410,7 @@
    1.15         if_True, if_False, if_cancel, if_eq_cancel,
    1.16         o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.17         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
    1.18 -       not1_or, not_all, not_ex, cases_simp]
    1.19 +       disj_not1, not_all, not_ex, cases_simp]
    1.20       @ ex_simps @ all_simps @ simp_thms)
    1.21       addsimprocs [defALL_regroup,defEX_regroup]
    1.22       addcongs [imp_cong];