src/HOL/Auth/OtwayRees_AN.ML

--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 15 15:10:38 1998 +0200
@@ -128,7 +128,7 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==>                                 \
-\  ALL K KK. KK <= Compl (range shrK) -->                \
+\  ALL K KK. KK <= -(range shrK) -->                  \
 \         (Key K : analz (Key``KK Un (spies evs))) =  \
 \         (K : KK | Key K : analz (spies evs))";
 by (etac otway.induct 1);