# HG changeset patch
# User paulson
# Date 992069018 -7200
# Node ID b42287eb20cfbe39a904c4c074237ac49d8d8043
# Parent  6d5698df0413ec4151cca68609e9798843d8e3e6
renaming of evs in the Fake rule

diff -r 6d5698df0413 -r b42287eb20cf src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Sat Jun 09 08:42:29 2001 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Sat Jun 09 08:43:38 2001 +0200
@@ -19,8 +19,8 @@
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-   Fake: "\<lbrakk>evs \<in> ns_public;  X \<in> synth (analz (spies evs))\<rbrakk>
-          \<Longrightarrow> Says Spy B X  # evs \<in> ns_public"
+   Fake: "\<lbrakk>evsf \<in> ns_public;  X \<in> synth (analz (spies evsf))\<rbrakk>
+          \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
    NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
diff -r 6d5698df0413 -r b42287eb20cf src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Sat Jun 09 08:42:29 2001 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Sat Jun 09 08:43:38 2001 +0200
@@ -23,8 +23,8 @@
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-   Fake: "\<lbrakk>evs \<in> ns_public;  X \<in> synth (analz (spies evs))\<rbrakk>
-          \<Longrightarrow> Says Spy B X  # evs \<in> ns_public"
+   Fake: "\<lbrakk>evsf \<in> ns_public;  X \<in> synth (analz (spies evsf))\<rbrakk>
+          \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
    NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>