# HG changeset patch
# User paulson
# Date 849808669 -3600
# Node ID 083912bc5775dc85026f5967559b9cea7d321dec
# Parent  41289907faedd1c2cd61f4a92ac4360e5912ea1f
Updated a comment

diff -r 41289907faed -r 083912bc5775 src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Thu Dec 05 18:57:29 1996 +0100
+++ b/src/HOL/Auth/WooLam.ML	Thu Dec 05 18:57:49 1996 +0100
@@ -17,7 +17,7 @@
 Pretty.setdepth 20;
 
 
-(*Weak liveness: there are traces that reach the end*)
+(*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX NB. EX evs: woolam.               \
@@ -137,7 +137,7 @@
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
                       addSEs [MPair_parts]
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "Server_trust_WL4";
+qed "Server_trusts_WL4";
 
 
 (*** WL5 ***)
@@ -179,9 +179,9 @@
  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
 \           A ~: lost;  B ~: lost;  evs : woolam  |] \
 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
-by (fast_tac (!claset addIs  [Server_trust_WL4]
+by (fast_tac (!claset addIs  [Server_trusts_WL4]
                       addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
-qed "B_trust_WL5";
+qed "B_trusts_WL5";
 
 
 (*B only issues challenges in response to WL1.  Useful??*)