# HG changeset patch
# User paulson
# Date 867746262 -7200
# Node ID 8160cc3f6d4003400f505a97c51e8d4896a83199
# Parent  61d927bd57ec89099d4e621cacc832c48cdc32b6
Added a comment

diff -r 61d927bd57ec -r 8160cc3f6d40 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Jul 01 10:37:03 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Tue Jul 01 10:37:42 1997 +0200
@@ -824,7 +824,9 @@
 
 (*** Tactics useful for many protocol proofs ***)
 
-(*Prove base case (subgoal i) and simplify others*)
+(*Prove base case (subgoal i) and simplify others.  A typical base case
+  concerns  Crypt K X ~: Key``shrK``lost  and cannot be proved by rewriting
+  alone.*)
 fun prove_simple_subgoals_tac i = 
     fast_tac (!claset addss (!simpset)) i THEN
     ALLGOALS Asm_simp_tac;
diff -r 61d927bd57ec -r 8160cc3f6d40 src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:03 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:42 1997 +0200
@@ -47,7 +47,10 @@
              Says B' A (Nonce NB) : set evs |]
           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
 
-         (*Bob forwards Alice's response to the Server.*)
+         (*Bob forwards Alice's response to the Server.  NOTE: usually
+           the messages are shown in chronological order, for clarity.
+           But here, exchanging the two events would cause the lemma
+           WL4_analz_sees_Spy to pick up the wrong assumption!*)
     WL4  "[| evs: woolam;  B ~= Server;  
              Says A'  B X         : set evs;
              Says A'' B (Agent A) : set evs |]