src/HOL/Auth/OtwayRees_AN.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5421 01fc8d6a40f2
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -18,8 +18,7 @@
     1.4  
     1.5  
     1.6  (*A "possibility property": there are traces that reach the end*)
     1.7 -Goal 
     1.8 - "[| A ~= B; A ~= Server; B ~= Server |]                               \
     1.9 +Goal "[| A ~= B; A ~= Server; B ~= Server |]                            \
    1.10  \  ==> EX K. EX NA. EX evs: otway.                                      \
    1.11  \       Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    1.12  \       : set evs";