# HG changeset patch
# User paulson
# Date 849864991 -3600
# Node ID e984c12ce5b4cea80cba291d6f87010582431c89
# Parent  00ac25b2791d225f8693eab00f18ad28a61543be
Minor renamings

diff -r 00ac25b2791d -r e984c12ce5b4 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Thu Dec 05 19:03:38 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Dec 06 10:36:31 1996 +0100
@@ -19,7 +19,7 @@
 Pretty.setdepth 15;
 
 
-(*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 K. EX NA. EX evs: otway lost.          \
@@ -364,9 +364,9 @@
   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   over-simplified version of this protocol: see OtwayRees_Bad.*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : otway lost |]                            \
+ "!!evs. [| A ~: lost;  evs : otway lost |]                      \
 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
-\             : parts (sees lost Spy evs) -->                       \
+\             : parts (sees lost Spy evs) -->                    \
 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
 \             ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
@@ -434,7 +434,7 @@
 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "A_trust_OR4";
+qed "A_trusts_OR4";
 
 
 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
@@ -590,10 +590,10 @@
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "B_trust_OR3";
+qed "B_trusts_OR3";
 
 
-B_trust_OR3 RS Spy_not_see_encrypted_key;
+B_trusts_OR3 RS Spy_not_see_encrypted_key;
 
 
 goal thy 
@@ -624,6 +624,6 @@
 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
 \            : set_of_list evs";
-by (fast_tac (!claset addSDs  [A_trust_OR4]
+by (fast_tac (!claset addSDs  [A_trusts_OR4]
                       addSEs [OR3_imp_OR2]) 1);
 qed "A_auths_B";