# HG changeset patch
# User nipkow
# Date 908358671 -7200
# Node ID b872b209db69397a0af869e9d60229162c0907da
# Parent  85fd64148873c329ddc7a13853283904ca1354c9
See (* FIXME zero_neq_conv *)

diff -r 85fd64148873 -r b872b209db69 src/HOL/Auth/TLS.ML
--- 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*)