src/HOL/Auth/Yahalom2.thy

--- a/src/HOL/Auth/Yahalom2.thy	Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Tue Sep 23 15:41:33 2003 +0200
@@ -80,14 +80,16 @@
 declare analz_into_parts [dest]
 
 text{*A "possibility property": there are traces that reach the end*}
-lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
+lemma "Key K \<notin> used []
+       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] yahalom.Nil
                     [THEN yahalom.YM1, THEN yahalom.Reception,
                      THEN yahalom.YM2, THEN yahalom.Reception,
                      THEN yahalom.YM3, THEN yahalom.Reception,
-                     THEN yahalom.YM4], possibility)
+                     THEN yahalom.YM4])
+apply (possibility, simp add: used_Cons) 
 done
 
 lemma Gets_imp_Says: