# HG changeset patch
# User paulson
# Date 1068631103 -3600
# Node ID 33e5ef9a4c98b879d8daed40ab9d9055b228c614
# Parent  e6e3e3f0deedd89316f032824e5151eb3e6cf000
tidied

diff -r e6e3e3f0deed -r 33e5ef9a4c98 src/HOL/SET-Protocol/Purchase.thy
--- a/src/HOL/SET-Protocol/Purchase.thy	Thu Nov 06 20:45:02 2003 +0100
+++ b/src/HOL/SET-Protocol/Purchase.thy	Wed Nov 12 10:58:23 2003 +0100
@@ -582,7 +582,7 @@
 lemma Nonce_compromise [rule_format (no_asm)]:
      "evs \<in> set_pur ==>
       (\<forall>N KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C))   -->
-              (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
+              (Nonce N \<in> analz (Key`KK \<union> (knows Spy evs))) =
               (Nonce N \<in> analz (knows Spy evs)))"
 apply (erule set_pur.induct)
 apply (rule_tac [!] allI)+
@@ -601,12 +601,13 @@
 done
 
 lemma PANSecret_notin_spies:
-     "evs \<in> set_pur
-   ==> Nonce (PANSecret k) \<in> analz (knows Spy evs) -->
+     "[|Nonce (PANSecret k) \<in> analz (knows Spy evs);  evs \<in> set_pur|]
+      ==> 
        (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.
           Says (Cardholder k) M
                {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
                  V|}  \<in>  set evs)"
+apply (erule rev_mp)
 apply (erule set_pur.induct)
 apply (frule_tac [9] AuthReq_msg_in_analz_spies)
 apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}