src/HOL/Auth/OtwayRees_Bad.ML

--- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Aug 06 15:48:13 1998 +0200
@@ -21,8 +21,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal 
- "[| A ~= B; A ~= Server; B ~= Server |]   \
+Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
 \  ==> EX K. EX NA. EX evs: otway.          \
 \         Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \           : set evs";