added not1_or and if_eq_cancel to simpset()
authoroheimb
Tue, 10 Mar 1998 18:32:08 +0100
changeset 4719 21af5c0be0c9
parent 4718 fc2ba9fb2135
child 4720 c1b83b42f65a
added not1_or and if_eq_cancel to simpset()
src/HOL/Auth/TLS.ML
src/HOL/Subst/Unifier.ML
src/HOL/TLA/Memory/Memory.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*) 
--- 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];
--- 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])
             ]);