# HG changeset patch
# User oheimb
# Date 889705033 -3600
# Node ID b3bfcbd9fb9304fd49c84c2860e3aac68269b6fc
# Parent  a25bb8a260ae63e5cfd196daed109e2eea5769c4
renamed not1_or to disj_not1, not2_or to disj_not2

diff -r a25bb8a260ae -r b3bfcbd9fb93 NEWS
--- a/NEWS	Thu Mar 12 13:15:36 1998 +0100
+++ b/NEWS	Thu Mar 12 13:17:13 1998 +0100
@@ -23,6 +23,8 @@
 
 *** HOL ***
 
+* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
+
 * HOL/Arithmetic: removed 'pred' (predecessor) function;
 
 * Simplifier:
diff -r a25bb8a260ae -r b3bfcbd9fb93 src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Thu Mar 12 13:15:36 1998 +0100
+++ b/src/HOL/TLA/Memory/Memory.ML	Thu Mar 12 13:17:13 1998 +0100
@@ -97,7 +97,7 @@
              ALLGOALS
 	        (action_simp_tac 
                     (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
-					WrRequest_def] delsimps [not1_or])
+					WrRequest_def] delsimps [disj_not1])
                     [] [base_enabled,Pair_inject])
             ]);
 
diff -r a25bb8a260ae -r b3bfcbd9fb93 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Mar 12 13:15:36 1998 +0100
+++ b/src/HOL/simpdata.ML	Thu Mar 12 13:17:13 1998 +0100
@@ -208,8 +208,8 @@
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
 prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
 prove "not_iff" "(P~=Q) = (P = (~Q))";
-prove "not1_or" "(~P | Q) = (P --> Q)";
-prove "not2_or" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
+prove "disj_not1" "(~P | Q) = (P --> Q)";
+prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
 
 (*Avoids duplication of subgoals after expand_if, when the true and false 
   cases boil down to the same thing.*) 
@@ -410,7 +410,7 @@
        if_True, if_False, if_cancel, if_eq_cancel,
        o_apply, imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
-       not1_or, not_all, not_ex, cases_simp]
+       disj_not1, not_all, not_ex, cases_simp]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong];