`` -> ` and ``` -> ``
authornipkow
Tue Jan 09 15:29:17 2001 +0100 (2001-01-09)
changeset 10833c0844a30ea4e
parent 10832 e33b47e4246d
child 10834 a7897aebbffc
`` -> ` and ``` -> ``
src/HOL/Algebra/abstract/Ideal.ML
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom_Bad.ML
     1.1 --- a/src/HOL/Algebra/abstract/Ideal.ML	Tue Jan 09 15:22:13 2001 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ideal.ML	Tue Jan 09 15:29:17 2001 +0100
     1.3 @@ -237,7 +237,7 @@
     1.4  qed_spec_mp "subset_chain_lemma";
     1.5  
     1.6  Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
     1.7 -\     ==> is_ideal (Union (I``UNIV))";
     1.8 +\     ==> is_ideal (Union (I`UNIV))";
     1.9  by (rtac is_idealI 1);
    1.10  by Auto_tac;
    1.11  by (res_inst_tac [("x", "max x xa")] exI 1);
    1.12 @@ -261,7 +261,7 @@
    1.13  
    1.14  (*
    1.15  Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
    1.16 -\   EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}";
    1.17 +\   EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}";
    1.18  
    1.19  Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
    1.20  by (simp_tac (simpset()
     2.1 --- a/src/HOL/Auth/KerberosIV.ML	Tue Jan 09 15:22:13 2001 +0100
     2.2 +++ b/src/HOL/Auth/KerberosIV.ML	Tue Jan 09 15:29:17 2001 +0100
     2.3 @@ -609,9 +609,9 @@
     2.4  
     2.5  (*We take some pains to express the property
     2.6    as a logical equivalence so that the simplifier can apply it.*)
     2.7 -Goal "P --> (Key K : analz (Key``KK Un H)) --> (K:KK | Key K : analz H)  \
     2.8 +Goal "P --> (Key K : analz (Key`KK Un H)) --> (K:KK | Key K : analz H)  \
     2.9  \     ==>       \
    2.10 -\     P --> (Key K : analz (Key``KK Un H)) = (K:KK | Key K : analz H)";
    2.11 +\     P --> (Key K : analz (Key`KK Un H)) = (K:KK | Key K : analz H)";
    2.12  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
    2.13  qed "Key_analz_image_Key_lemma";
    2.14  
    2.15 @@ -651,7 +651,7 @@
    2.16  		  ORELSE' hyp_subst_tac)];
    2.17  
    2.18  Goal "[| KK <= -(range shrK); Key K : analz (spies evs); evs: kerberos |]   \
    2.19 -\     ==> Key K : analz (Key `` KK Un spies evs)";
    2.20 +\     ==> Key K : analz (Key ` KK Un spies evs)";
    2.21  by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
    2.22  qed "analz_mono_KK";
    2.23  
    2.24 @@ -673,7 +673,7 @@
    2.25  Goal "evs : kerberos ==>                                         \
    2.26  \     (ALL SK KK. KK <= -(range shrK) -->                   \
    2.27  \     (ALL K: KK. ~ KeyCryptKey K SK evs)   -->           \
    2.28 -\     (Key SK : analz (Key``KK Un (spies evs))) =        \
    2.29 +\     (Key SK : analz (Key`KK Un (spies evs))) =        \
    2.30  \     (SK : KK | Key SK : analz (spies evs)))";
    2.31  by (etac kerberos.induct 1);
    2.32  by analz_sees_tac;
     3.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Jan 09 15:22:13 2001 +0100
     3.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Tue Jan 09 15:29:17 2001 +0100
     3.3 @@ -180,7 +180,7 @@
     3.4  
     3.5  Goal "evs : kerberos_ban ==>                          \
     3.6  \  ALL K KK. KK <= - (range shrK) -->                 \
     3.7 -\         (Key K : analz (Key``KK Un (spies evs))) =  \
     3.8 +\         (Key K : analz (Key`KK Un (spies evs))) =  \
     3.9  \         (K : KK | Key K : analz (spies evs))";
    3.10  by (etac kerberos_ban.induct 1);
    3.11  by analz_spies_tac;
     4.1 --- a/src/HOL/Auth/Message.ML	Tue Jan 09 15:22:13 2001 +0100
     4.2 +++ b/src/HOL/Auth/Message.ML	Tue Jan 09 15:29:17 2001 +0100
     4.3 @@ -16,15 +16,15 @@
     4.4  AddIffs msg.inject;
     4.5  
     4.6  (*Equations hold because constructors are injective; cannot prove for all f*)
     4.7 -Goal "(Friend x : Friend``A) = (x:A)";
     4.8 +Goal "(Friend x : Friend`A) = (x:A)";
     4.9  by Auto_tac;
    4.10  qed "Friend_image_eq";
    4.11  
    4.12 -Goal "(Key x : Key``A) = (x:A)";
    4.13 +Goal "(Key x : Key`A) = (x:A)";
    4.14  by Auto_tac;
    4.15  qed "Key_image_eq";
    4.16  
    4.17 -Goal "(Nonce x ~: Key``A)";
    4.18 +Goal "(Nonce x ~: Key`A)";
    4.19  by Auto_tac;
    4.20  qed "Nonce_Key_image_eq";
    4.21  Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
    4.22 @@ -97,7 +97,7 @@
    4.23  AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
    4.24  	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
    4.25  
    4.26 -Goalw [keysFor_def] "keysFor (Key``E) = {}";
    4.27 +Goalw [keysFor_def] "keysFor (Key`E) = {}";
    4.28  by Auto_tac;
    4.29  qed "keysFor_image_Key";
    4.30  Addsimps [keysFor_image_Key];
    4.31 @@ -296,7 +296,7 @@
    4.32            parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
    4.33  
    4.34  
    4.35 -Goal "parts (Key``N) = Key``N";
    4.36 +Goal "parts (Key`N) = Key`N";
    4.37  by Auto_tac;
    4.38  by (etac parts.induct 1);
    4.39  by Auto_tac;
    4.40 @@ -484,7 +484,7 @@
    4.41  qed "analz_insert_Crypt_subset";
    4.42  
    4.43  
    4.44 -Goal "analz (Key``N) = Key``N";
    4.45 +Goal "analz (Key`N) = Key`N";
    4.46  by Auto_tac;
    4.47  by (etac analz.induct 1);
    4.48  by Auto_tac;
    4.49 @@ -653,7 +653,7 @@
    4.50  
    4.51  
    4.52  Goalw [keysFor_def]
    4.53 -    "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
    4.54 +    "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}";
    4.55  by (Blast_tac 1);
    4.56  qed "keysFor_synth";
    4.57  Addsimps [keysFor_synth];
    4.58 @@ -707,7 +707,7 @@
    4.59  by (Blast_tac 1);
    4.60  qed "Fake_parts_insert";
    4.61  
    4.62 -(*H is sometimes (Key `` KK Un spies evs), so can't put G=H*)
    4.63 +(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
    4.64  Goal "X: synth (analz G) ==> \
    4.65  \     analz (insert X H) <= synth (analz G) Un analz (G Un H)";
    4.66  by (rtac subsetI 1);
    4.67 @@ -853,7 +853,7 @@
    4.68  (*** Tactics useful for many protocol proofs ***)
    4.69  
    4.70  (*Prove base case (subgoal i) and simplify others.  A typical base case
    4.71 -  concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
    4.72 +  concerns  Crypt K X ~: Key`shrK`bad  and cannot be proved by rewriting
    4.73    alone.*)
    4.74  fun prove_simple_subgoals_tac i = 
    4.75      force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
     5.1 --- a/src/HOL/Auth/Message.thy	Tue Jan 09 15:22:13 2001 +0100
     5.2 +++ b/src/HOL/Auth/Message.thy	Tue Jan 09 15:29:17 2001 +0100
     5.3 @@ -57,7 +57,7 @@
     5.4  
     5.5    (*Keys useful to decrypt elements of a message set*)
     5.6    keysFor :: msg set => key set
     5.7 -  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
     5.8 +  "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
     5.9  
    5.10  (** Inductive definition of all "parts" of a message.  **)
    5.11  
     6.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Jan 09 15:22:13 2001 +0100
     6.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Jan 09 15:29:17 2001 +0100
     6.3 @@ -175,7 +175,7 @@
     6.4  (*The equality makes the induction hypothesis easier to apply*)
     6.5  Goal "evs : ns_shared ==>                             \
     6.6  \  ALL K KK. KK <= - (range shrK) -->                 \
     6.7 -\            (Key K : analz (Key``KK Un (spies evs))) =  \
     6.8 +\            (Key K : analz (Key`KK Un (spies evs))) =  \
     6.9  \            (K : KK | Key K : analz (spies evs))";
    6.10  by (etac ns_shared.induct 1);
    6.11  by analz_spies_tac;
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Jan 09 15:22:13 2001 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Jan 09 15:29:17 2001 +0100
     7.3 @@ -148,7 +148,7 @@
     7.4  
     7.5  (*The equality makes the induction hypothesis easier to apply*)
     7.6  Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) -->           \
     7.7 -\                      (Key K : analz (Key``KK Un (knows Spy evs))) =  \
     7.8 +\                      (Key K : analz (Key`KK Un (knows Spy evs))) =  \
     7.9  \                      (K : KK | Key K : analz (knows Spy evs))";
    7.10  by (etac otway.induct 1);
    7.11  by analz_knows_Spy_tac;
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Jan 09 15:22:13 2001 +0100
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Jan 09 15:29:17 2001 +0100
     8.3 @@ -142,7 +142,7 @@
     8.4  (*The equality makes the induction hypothesis easier to apply*)
     8.5  Goal "evs : otway ==>                                 \
     8.6  \  ALL K KK. KK <= -(range shrK) -->                  \
     8.7 -\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
     8.8 +\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
     8.9  \         (K : KK | Key K : analz (knows Spy evs))";
    8.10  by (etac otway.induct 1);
    8.11  by analz_knows_Spy_tac;
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Jan 09 15:22:13 2001 +0100
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Jan 09 15:29:17 2001 +0100
     9.3 @@ -153,7 +153,7 @@
     9.4  (*The equality makes the induction hypothesis easier to apply*)
     9.5  Goal "evs : otway ==>                                 \
     9.6  \  ALL K KK. KK <= - (range shrK) -->                 \
     9.7 -\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
     9.8 +\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
     9.9  \         (K : KK | Key K : analz (knows Spy evs))";
    9.10  by (etac otway.induct 1);
    9.11  by analz_knows_Spy_tac;
    10.1 --- a/src/HOL/Auth/Public.ML	Tue Jan 09 15:22:13 2001 +0100
    10.2 +++ b/src/HOL/Auth/Public.ML	Tue Jan 09 15:29:17 2001 +0100
    10.3 @@ -34,16 +34,16 @@
    10.4  
    10.5  (** "Image" equations that hold for injective functions **)
    10.6  
    10.7 -Goal "(invKey x : invKey``A) = (x:A)";
    10.8 +Goal "(invKey x : invKey`A) = (x:A)";
    10.9  by Auto_tac;
   10.10  qed "invKey_image_eq";
   10.11  
   10.12  (*holds because invKey is injective*)
   10.13 -Goal "(pubK x : pubK``A) = (x:A)";
   10.14 +Goal "(pubK x : pubK`A) = (x:A)";
   10.15  by Auto_tac;
   10.16  qed "pubK_image_eq";
   10.17  
   10.18 -Goal "(priK x ~: pubK``A)";
   10.19 +Goal "(priK x ~: pubK`A)";
   10.20  by Auto_tac;
   10.21  qed "priK_pubK_image_eq";
   10.22  Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
   10.23 @@ -157,11 +157,11 @@
   10.24  
   10.25  (*** Specialized rewriting for the analz_image_... theorems ***)
   10.26  
   10.27 -Goal "insert (Key K) H = Key `` {K} Un H";
   10.28 +Goal "insert (Key K) H = Key ` {K} Un H";
   10.29  by (Blast_tac 1);
   10.30  qed "insert_Key_singleton";
   10.31  
   10.32 -Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   10.33 +Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
   10.34  by (Blast_tac 1);
   10.35  qed "insert_Key_image";
   10.36  
    11.1 --- a/src/HOL/Auth/Public.thy	Tue Jan 09 15:22:13 2001 +0100
    11.2 +++ b/src/HOL/Auth/Public.thy	Tue Jan 09 15:29:17 2001 +0100
    11.3 @@ -22,11 +22,11 @@
    11.4  primrec
    11.5          (*Agents know their private key and all public keys*)
    11.6    initState_Server  "initState Server     =    
    11.7 - 		         insert (Key (priK Server)) (Key `` range pubK)"
    11.8 + 		         insert (Key (priK Server)) (Key ` range pubK)"
    11.9    initState_Friend  "initState (Friend i) =    
   11.10 - 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
   11.11 + 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
   11.12    initState_Spy     "initState Spy        =    
   11.13 - 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
   11.14 + 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
   11.15  
   11.16  
   11.17  rules
    12.1 --- a/src/HOL/Auth/Recur.ML	Tue Jan 09 15:22:13 2001 +0100
    12.2 +++ b/src/HOL/Auth/Recur.ML	Tue Jan 09 15:29:17 2001 +0100
    12.3 @@ -186,10 +186,10 @@
    12.4    satisfying the inductive hypothesis.*)
    12.5  Goal "[| RB : responses evs;                             \
    12.6  \        ALL K KK. KK <= - (range shrK) -->              \
    12.7 -\                  (Key K : analz (Key``KK Un H)) =      \
    12.8 +\                  (Key K : analz (Key`KK Un H)) =      \
    12.9  \                  (K : KK | Key K : analz H) |]         \
   12.10  \    ==> ALL K KK. KK <= - (range shrK) -->              \
   12.11 -\                  (Key K : analz (insert RB (Key``KK Un H))) = \
   12.12 +\                  (Key K : analz (insert RB (Key`KK Un H))) = \
   12.13  \                  (K : KK | Key K : analz (insert RB H))";
   12.14  by (etac responses.induct 1);
   12.15  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   12.16 @@ -198,7 +198,7 @@
   12.17  (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
   12.18  Goal "evs : recur ==>                                 \
   12.19  \  ALL K KK. KK <= - (range shrK) -->                 \
   12.20 -\         (Key K : analz (Key``KK Un (spies evs))) =  \
   12.21 +\         (Key K : analz (Key`KK Un (spies evs))) =  \
   12.22  \         (K : KK | Key K : analz (spies evs))";
   12.23  by (etac recur.induct 1);
   12.24  by analz_spies_tac;
   12.25 @@ -216,7 +216,7 @@
   12.26  (*Instance of the lemma with H replaced by (spies evs):
   12.27     [| RB : responses evs;  evs : recur; |]
   12.28     ==> KK <= - (range shrK) --> 
   12.29 -       Key K : analz (insert RB (Key``KK Un spies evs)) =
   12.30 +       Key K : analz (insert RB (Key`KK Un spies evs)) =
   12.31         (K : KK | Key K : analz (insert RB (spies evs))) 
   12.32  *)
   12.33  bind_thm ("resp_analz_image_freshK",
   12.34 @@ -291,7 +291,7 @@
   12.35  
   12.36  Goal "[| RB : responses evs;                         \
   12.37  \        ALL K KK. KK <= - (range shrK) -->          \
   12.38 -\                  (Key K : analz (Key``KK Un H)) =  \
   12.39 +\                  (Key K : analz (Key`KK Un H)) =  \
   12.40  \                  (K : KK | Key K : analz H) |]     \
   12.41  \    ==> (Key K : analz (insert RB H)) -->           \
   12.42  \        (Key K : parts{RB} | Key K : analz H)";
    13.1 --- a/src/HOL/Auth/Shared.ML	Tue Jan 09 15:22:13 2001 +0100
    13.2 +++ b/src/HOL/Auth/Shared.ML	Tue Jan 09 15:29:17 2001 +0100
    13.3 @@ -223,11 +223,11 @@
    13.4  by (Blast_tac 1);
    13.5  qed "subset_Compl_range";
    13.6  
    13.7 -Goal "insert (Key K) H = Key `` {K} Un H";
    13.8 +Goal "insert (Key K) H = Key ` {K} Un H";
    13.9  by (Blast_tac 1);
   13.10  qed "insert_Key_singleton";
   13.11  
   13.12 -Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   13.13 +Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
   13.14  by (Blast_tac 1);
   13.15  qed "insert_Key_image";
   13.16  
   13.17 @@ -244,7 +244,7 @@
   13.18  			@disj_comms;
   13.19  
   13.20  (*Lemma for the trivial direction of the if-and-only-if*)
   13.21 -Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
   13.22 -\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
   13.23 +Goal "(Key K : analz (Key`nE Un H)) --> (K : nE | Key K : analz H)  ==> \
   13.24 +\        (Key K : analz (Key`nE Un H)) = (K : nE | Key K : analz H)";
   13.25  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   13.26  qed "analz_image_freshK_lemma";
    14.1 --- a/src/HOL/Auth/Shared.thy	Tue Jan 09 15:22:13 2001 +0100
    14.2 +++ b/src/HOL/Auth/Shared.thy	Tue Jan 09 15:29:17 2001 +0100
    14.3 @@ -19,9 +19,9 @@
    14.4  
    14.5  primrec
    14.6          (*Server knows all long-term keys; other agents know only their own*)
    14.7 -  initState_Server  "initState Server     = Key `` range shrK"
    14.8 +  initState_Server  "initState Server     = Key ` range shrK"
    14.9    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
   14.10 -  initState_Spy     "initState Spy        = Key``shrK``bad"
   14.11 +  initState_Spy     "initState Spy        = Key`shrK`bad"
   14.12  
   14.13  
   14.14  rules
    15.1 --- a/src/HOL/Auth/TLS.ML	Tue Jan 09 15:22:13 2001 +0100
    15.2 +++ b/src/HOL/Auth/TLS.ML	Tue Jan 09 15:29:17 2001 +0100
    15.3 @@ -334,7 +334,7 @@
    15.4  (*Key compromise lemma needed to prove analz_image_keys.
    15.5    No collection of keys can help the spy get new private keys.*)
    15.6  Goal "evs : tls                                      \
    15.7 -\     ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
    15.8 +\     ==> ALL KK. (Key(priK B) : analz (Key`KK Un (spies evs))) = \
    15.9  \         (priK B : KK | B : bad)";
   15.10  by (etac tls.induct 1);
   15.11  by (ALLGOALS
   15.12 @@ -357,13 +357,13 @@
   15.13  val analz_image_keys_lemma = result();
   15.14  
   15.15  (** Strangely, the following version doesn't work:
   15.16 -\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   15.17 +\ ALL Z. (Nonce N : analz (Key`(sessionK`Z) Un (spies evs))) = \
   15.18  \        (Nonce N : analz (spies evs))";
   15.19  **)
   15.20  
   15.21  Goal "evs : tls ==>                                    \
   15.22  \ ALL KK. KK <= range sessionK -->                     \
   15.23 -\         (Nonce N : analz (Key``KK Un (spies evs))) = \
   15.24 +\         (Nonce N : analz (Key`KK Un (spies evs))) = \
   15.25  \         (Nonce N : analz (spies evs))";
   15.26  by (etac tls.induct 1);
   15.27  by (ClientKeyExch_tac 7);
    16.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Jan 09 15:22:13 2001 +0100
    16.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Jan 09 15:29:17 2001 +0100
    16.3 @@ -147,7 +147,7 @@
    16.4  
    16.5  Goal "evs : yahalom ==>                              \
    16.6  \  ALL K KK. KK <= - (range shrK) -->                \
    16.7 -\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
    16.8 +\         (Key K : analz (Key`KK Un (knows Spy evs))) = \
    16.9  \         (K : KK | Key K : analz (knows Spy evs))";
   16.10  by (etac yahalom.induct 1);
   16.11  by analz_knows_Spy_tac;
   16.12 @@ -367,7 +367,7 @@
   16.13  Goal "evs : yahalom ==>                                      \
   16.14  \     (ALL KK. KK <= - (range shrK) -->                      \
   16.15  \          (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
   16.16 -\          (Nonce NB : analz (Key``KK Un (knows Spy evs))) =     \
   16.17 +\          (Nonce NB : analz (Key`KK Un (knows Spy evs))) =     \
   16.18  \          (Nonce NB : analz (knows Spy evs)))";
   16.19  by (etac yahalom.induct 1);
   16.20  by analz_knows_Spy_tac;
    17.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Jan 09 15:22:13 2001 +0100
    17.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Jan 09 15:29:17 2001 +0100
    17.3 @@ -149,7 +149,7 @@
    17.4  
    17.5  Goal "evs : yahalom ==>                               \
    17.6  \  ALL K KK. KK <= - (range shrK) -->                 \
    17.7 -\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
    17.8 +\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
    17.9  \         (K : KK | Key K : analz (knows Spy evs))";
   17.10  by (etac yahalom.induct 1);
   17.11  by analz_knows_Spy_tac;
    18.1 --- a/src/HOL/Auth/Yahalom_Bad.ML	Tue Jan 09 15:22:13 2001 +0100
    18.2 +++ b/src/HOL/Auth/Yahalom_Bad.ML	Tue Jan 09 15:29:17 2001 +0100
    18.3 @@ -122,7 +122,7 @@
    18.4  
    18.5  Goal "evs : yahalom ==>                              \
    18.6  \  ALL K KK. KK <= - (range shrK) -->                \
    18.7 -\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
    18.8 +\         (Key K : analz (Key`KK Un (knows Spy evs))) = \
    18.9  \         (K : KK | Key K : analz (knows Spy evs))";
   18.10  by (etac yahalom.induct 1);
   18.11  by analz_knows_Spy_tac;