--- 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])
]);