--- a/src/HOL/Auth/TLS.ML Wed Oct 14 11:50:48 1998 +0200
+++ b/src/HOL/Auth/TLS.ML Wed Oct 14 11:51:11 1998 +0200
@@ -526,9 +526,12 @@
\ ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
+(* FIXME zero_neq_conv *)
+DelIffs [zero_neq_conv];
by (analz_induct_tac 1); (*17 seconds*)
(*Oops*)
by (blast_tac (claset() addIs [Says_clientK_unique]) 4);
+AddIffs [zero_neq_conv];
(*ClientKeyExch*)
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3);
(*SpyKeys*)