# HG changeset patch
# User oheimb
# Date 889551128 -3600
# Node ID 21af5c0be0c93bade2eabc9f8ea80683621a840b
# Parent  fc2ba9fb21356e06a6bc73cef277f9410c835dd4
added not1_or and if_eq_cancel to simpset()

diff -r fc2ba9fb2135 -r 21af5c0be0c9 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Tue Mar 10 18:31:32 1998 +0100
+++ b/src/HOL/Auth/TLS.ML	Tue Mar 10 18:32:08 1998 +0100
@@ -480,8 +480,6 @@
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (analz_induct_tac 1);        (*17 seconds*)
-(*Oops*)
-by (Blast_tac 4);
 (*SpyKeys*)
 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
 (*Fake*) 
diff -r fc2ba9fb2135 -r 21af5c0be0c9 src/HOL/Subst/Unifier.ML
--- a/src/HOL/Subst/Unifier.ML	Tue Mar 10 18:31:32 1998 +0100
+++ b/src/HOL/Subst/Unifier.ML	Tue Mar 10 18:32:08 1998 +0100
@@ -82,8 +82,7 @@
 
 goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
 by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
-				 empty_iff_all_not]) 1);
-by (Blast_tac 1);
+				  empty_iff_all_not]) 1);
 qed_spec_mp "Var_Idem";
 
 AddSIs [Var_Idem];
diff -r fc2ba9fb2135 -r 21af5c0be0c9 src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Tue Mar 10 18:31:32 1998 +0100
+++ b/src/HOL/TLA/Memory/Memory.ML	Tue Mar 10 18:32:08 1998 +0100
@@ -97,7 +97,7 @@
              ALLGOALS
 	        (action_simp_tac 
                     (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
-					WrRequest_def])
+					WrRequest_def] delsimps [not1_or])
                     [] [base_enabled,Pair_inject])
             ]);