src/HOL/Auth/OtwayRees_Bad.ML

 
 (** Session keys are not used to encrypt other session keys **)
 
 (*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);
 by analz_spies_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));