changeset 10833 | c0844a30ea4e |
parent 9165 | f46f407080f8 |
--- a/src/HOL/Auth/NS_Shared.ML Tue Jan 09 15:22:13 2001 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Tue Jan 09 15:29:17 2001 +0100 @@ -175,7 +175,7 @@ (*The equality makes the induction hypothesis easier to apply*) Goal "evs : ns_shared ==> \ \ ALL K KK. KK <= - (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ +\ (Key K : analz (Key`KK Un (spies evs))) = \ \ (K : KK | Key K : analz (spies evs))"; by (etac ns_shared.induct 1); by analz_spies_tac;