renamed not1_or to disj_not1, not2_or to disj_not2
authoroheimb
Thu Mar 12 13:17:13 1998 +0100 (1998-03-12)
changeset 4743b3bfcbd9fb93
parent 4742 a25bb8a260ae
child 4744 4469d498cd48
renamed not1_or to disj_not1, not2_or to disj_not2
NEWS
src/HOL/TLA/Memory/Memory.ML
src/HOL/simpdata.ML
     1.1 --- a/NEWS	Thu Mar 12 13:15:36 1998 +0100
     1.2 +++ b/NEWS	Thu Mar 12 13:17:13 1998 +0100
     1.3 @@ -23,6 +23,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
     1.8 +
     1.9  * HOL/Arithmetic: removed 'pred' (predecessor) function;
    1.10  
    1.11  * Simplifier:
     2.1 --- a/src/HOL/TLA/Memory/Memory.ML	Thu Mar 12 13:15:36 1998 +0100
     2.2 +++ b/src/HOL/TLA/Memory/Memory.ML	Thu Mar 12 13:17:13 1998 +0100
     2.3 @@ -97,7 +97,7 @@
     2.4               ALLGOALS
     2.5  	        (action_simp_tac 
     2.6                      (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
     2.7 -					WrRequest_def] delsimps [not1_or])
     2.8 +					WrRequest_def] delsimps [disj_not1])
     2.9                      [] [base_enabled,Pair_inject])
    2.10              ]);
    2.11  
     3.1 --- a/src/HOL/simpdata.ML	Thu Mar 12 13:15:36 1998 +0100
     3.2 +++ b/src/HOL/simpdata.ML	Thu Mar 12 13:17:13 1998 +0100
     3.3 @@ -208,8 +208,8 @@
     3.4  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
     3.5  prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
     3.6  prove "not_iff" "(P~=Q) = (P = (~Q))";
     3.7 -prove "not1_or" "(~P | Q) = (P --> Q)";
     3.8 -prove "not2_or" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
     3.9 +prove "disj_not1" "(~P | Q) = (P --> Q)";
    3.10 +prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
    3.11  
    3.12  (*Avoids duplication of subgoals after expand_if, when the true and false 
    3.13    cases boil down to the same thing.*) 
    3.14 @@ -410,7 +410,7 @@
    3.15         if_True, if_False, if_cancel, if_eq_cancel,
    3.16         o_apply, imp_disjL, conj_assoc, disj_assoc,
    3.17         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
    3.18 -       not1_or, not_all, not_ex, cases_simp]
    3.19 +       disj_not1, not_all, not_ex, cases_simp]
    3.20       @ ex_simps @ all_simps @ simp_thms)
    3.21       addsimprocs [defALL_regroup,defEX_regroup]
    3.22       addcongs [imp_cong];