src/HOL/Auth/OtwayRees_Bad.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5421 01fc8d6a40f2
     1.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -21,8 +21,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 {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    1.12  \           : set evs";