# HG changeset patch
# User nipkow
# Date 979050557 -3600
# Node ID c0844a30ea4ea5a7834325c9ba33e18d8f5ed6af
# Parent  e33b47e4246d9903cadd57c1afaf662343026eed
`` -> ` and ``` -> ``

diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Algebra/abstract/Ideal.ML
--- a/src/HOL/Algebra/abstract/Ideal.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -237,7 +237,7 @@
 qed_spec_mp "subset_chain_lemma";
 
 Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
-\     ==> is_ideal (Union (I``UNIV))";
+\     ==> is_ideal (Union (I`UNIV))";
 by (rtac is_idealI 1);
 by Auto_tac;
 by (res_inst_tac [("x", "max x xa")] exI 1);
@@ -261,7 +261,7 @@
 
 (*
 Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
-\   EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}";
+\   EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}";
 
 Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
 by (simp_tac (simpset()
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/KerberosIV.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -609,9 +609,9 @@
 
 (*We take some pains to express the property
   as a logical equivalence so that the simplifier can apply it.*)
-Goal "P --> (Key K : analz (Key``KK Un H)) --> (K:KK | Key K : analz H)  \
+Goal "P --> (Key K : analz (Key`KK Un H)) --> (K:KK | Key K : analz H)  \
 \     ==>       \
-\     P --> (Key K : analz (Key``KK Un H)) = (K:KK | Key K : analz H)";
+\     P --> (Key K : analz (Key`KK Un H)) = (K:KK | Key K : analz H)";
 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
 qed "Key_analz_image_Key_lemma";
 
@@ -651,7 +651,7 @@
 		  ORELSE' hyp_subst_tac)];
 
 Goal "[| KK <= -(range shrK); Key K : analz (spies evs); evs: kerberos |]   \
-\     ==> Key K : analz (Key `` KK Un spies evs)";
+\     ==> Key K : analz (Key ` KK Un spies evs)";
 by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
 qed "analz_mono_KK";
 
@@ -673,7 +673,7 @@
 Goal "evs : kerberos ==>                                         \
 \     (ALL SK KK. KK <= -(range shrK) -->                   \
 \     (ALL K: KK. ~ KeyCryptKey K SK evs)   -->           \
-\     (Key SK : analz (Key``KK Un (spies evs))) =        \
+\     (Key SK : analz (Key`KK Un (spies evs))) =        \
 \     (SK : KK | Key SK : analz (spies evs)))";
 by (etac kerberos.induct 1);
 by analz_sees_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -180,7 +180,7 @@
 
 Goal "evs : kerberos_ban ==>                          \
 \  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 kerberos_ban.induct 1);
 by analz_spies_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Message.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -16,15 +16,15 @@
 AddIffs msg.inject;
 
 (*Equations hold because constructors are injective; cannot prove for all f*)
-Goal "(Friend x : Friend``A) = (x:A)";
+Goal "(Friend x : Friend`A) = (x:A)";
 by Auto_tac;
 qed "Friend_image_eq";
 
-Goal "(Key x : Key``A) = (x:A)";
+Goal "(Key x : Key`A) = (x:A)";
 by Auto_tac;
 qed "Key_image_eq";
 
-Goal "(Nonce x ~: Key``A)";
+Goal "(Nonce x ~: Key`A)";
 by Auto_tac;
 qed "Nonce_Key_image_eq";
 Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
@@ -97,7 +97,7 @@
 AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
 	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
 
-Goalw [keysFor_def] "keysFor (Key``E) = {}";
+Goalw [keysFor_def] "keysFor (Key`E) = {}";
 by Auto_tac;
 qed "keysFor_image_Key";
 Addsimps [keysFor_image_Key];
@@ -296,7 +296,7 @@
           parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
 
 
-Goal "parts (Key``N) = Key``N";
+Goal "parts (Key`N) = Key`N";
 by Auto_tac;
 by (etac parts.induct 1);
 by Auto_tac;
@@ -484,7 +484,7 @@
 qed "analz_insert_Crypt_subset";
 
 
-Goal "analz (Key``N) = Key``N";
+Goal "analz (Key`N) = Key`N";
 by Auto_tac;
 by (etac analz.induct 1);
 by Auto_tac;
@@ -653,7 +653,7 @@
 
 
 Goalw [keysFor_def]
-    "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
+    "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}";
 by (Blast_tac 1);
 qed "keysFor_synth";
 Addsimps [keysFor_synth];
@@ -707,7 +707,7 @@
 by (Blast_tac 1);
 qed "Fake_parts_insert";
 
-(*H is sometimes (Key `` KK Un spies evs), so can't put G=H*)
+(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
 Goal "X: synth (analz G) ==> \
 \     analz (insert X H) <= synth (analz G) Un analz (G Un H)";
 by (rtac subsetI 1);
@@ -853,7 +853,7 @@
 (*** Tactics useful for many protocol proofs ***)
 
 (*Prove base case (subgoal i) and simplify others.  A typical base case
-  concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
+  concerns  Crypt K X ~: Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
     force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Message.thy	Tue Jan 09 15:29:17 2001 +0100
@@ -57,7 +57,7 @@
 
   (*Keys useful to decrypt elements of a message set*)
   keysFor :: msg set => key set
-  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
+  "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
 
 (** Inductive definition of all "parts" of a message.  **)
 
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/NS_Shared.ML
--- 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;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -148,7 +148,7 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) -->           \
-\                      (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\                      (Key K : analz (Key`KK Un (knows Spy evs))) =  \
 \                      (K : KK | Key K : analz (knows Spy evs))";
 by (etac otway.induct 1);
 by analz_knows_Spy_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -142,7 +142,7 @@
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==>                                 \
 \  ALL K KK. KK <= -(range shrK) -->                  \
-\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
 \         (K : KK | Key K : analz (knows Spy evs))";
 by (etac otway.induct 1);
 by analz_knows_Spy_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -153,7 +153,7 @@
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==>                                 \
 \  ALL K KK. KK <= - (range shrK) -->                 \
-\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
 \         (K : KK | Key K : analz (knows Spy evs))";
 by (etac otway.induct 1);
 by analz_knows_Spy_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Public.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -34,16 +34,16 @@
 
 (** "Image" equations that hold for injective functions **)
 
-Goal "(invKey x : invKey``A) = (x:A)";
+Goal "(invKey x : invKey`A) = (x:A)";
 by Auto_tac;
 qed "invKey_image_eq";
 
 (*holds because invKey is injective*)
-Goal "(pubK x : pubK``A) = (x:A)";
+Goal "(pubK x : pubK`A) = (x:A)";
 by Auto_tac;
 qed "pubK_image_eq";
 
-Goal "(priK x ~: pubK``A)";
+Goal "(priK x ~: pubK`A)";
 by Auto_tac;
 qed "priK_pubK_image_eq";
 Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
@@ -157,11 +157,11 @@
 
 (*** Specialized rewriting for the analz_image_... theorems ***)
 
-Goal "insert (Key K) H = Key `` {K} Un H";
+Goal "insert (Key K) H = Key ` {K} Un H";
 by (Blast_tac 1);
 qed "insert_Key_singleton";
 
-Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
+Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
 by (Blast_tac 1);
 qed "insert_Key_image";
 
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Public.thy	Tue Jan 09 15:29:17 2001 +0100
@@ -22,11 +22,11 @@
 primrec
         (*Agents know their private key and all public keys*)
   initState_Server  "initState Server     =    
- 		         insert (Key (priK Server)) (Key `` range pubK)"
+ 		         insert (Key (priK Server)) (Key ` range pubK)"
   initState_Friend  "initState (Friend i) =    
- 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
+ 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
   initState_Spy     "initState Spy        =    
- 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
+ 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
 
 
 rules
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Recur.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -186,10 +186,10 @@
   satisfying the inductive hypothesis.*)
 Goal "[| RB : responses evs;                             \
 \        ALL K KK. KK <= - (range shrK) -->              \
-\                  (Key K : analz (Key``KK Un H)) =      \
+\                  (Key K : analz (Key`KK Un H)) =      \
 \                  (K : KK | Key K : analz H) |]         \
 \    ==> ALL K KK. KK <= - (range shrK) -->              \
-\                  (Key K : analz (insert RB (Key``KK Un H))) = \
+\                  (Key K : analz (insert RB (Key`KK Un H))) = \
 \                  (K : KK | Key K : analz (insert RB H))";
 by (etac responses.induct 1);
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -198,7 +198,7 @@
 (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
 Goal "evs : recur ==>                                 \
 \  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 recur.induct 1);
 by analz_spies_tac;
@@ -216,7 +216,7 @@
 (*Instance of the lemma with H replaced by (spies evs):
    [| RB : responses evs;  evs : recur; |]
    ==> KK <= - (range shrK) --> 
-       Key K : analz (insert RB (Key``KK Un spies evs)) =
+       Key K : analz (insert RB (Key`KK Un spies evs)) =
        (K : KK | Key K : analz (insert RB (spies evs))) 
 *)
 bind_thm ("resp_analz_image_freshK",
@@ -291,7 +291,7 @@
 
 Goal "[| RB : responses evs;                         \
 \        ALL K KK. KK <= - (range shrK) -->          \
-\                  (Key K : analz (Key``KK Un H)) =  \
+\                  (Key K : analz (Key`KK Un H)) =  \
 \                  (K : KK | Key K : analz H) |]     \
 \    ==> (Key K : analz (insert RB H)) -->           \
 \        (Key K : parts{RB} | Key K : analz H)";
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Shared.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -223,11 +223,11 @@
 by (Blast_tac 1);
 qed "subset_Compl_range";
 
-Goal "insert (Key K) H = Key `` {K} Un H";
+Goal "insert (Key K) H = Key ` {K} Un H";
 by (Blast_tac 1);
 qed "insert_Key_singleton";
 
-Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
+Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
 by (Blast_tac 1);
 qed "insert_Key_image";
 
@@ -244,7 +244,7 @@
 			@disj_comms;
 
 (*Lemma for the trivial direction of the if-and-only-if*)
-Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
-\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
+Goal "(Key K : analz (Key`nE Un H)) --> (K : nE | Key K : analz H)  ==> \
+\        (Key K : analz (Key`nE Un H)) = (K : nE | Key K : analz H)";
 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
 qed "analz_image_freshK_lemma";
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Shared.thy	Tue Jan 09 15:29:17 2001 +0100
@@ -19,9 +19,9 @@
 
 primrec
         (*Server knows all long-term keys; other agents know only their own*)
-  initState_Server  "initState Server     = Key `` range shrK"
+  initState_Server  "initState Server     = Key ` range shrK"
   initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
-  initState_Spy     "initState Spy        = Key``shrK``bad"
+  initState_Spy     "initState Spy        = Key`shrK`bad"
 
 
 rules
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/TLS.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -334,7 +334,7 @@
 (*Key compromise lemma needed to prove analz_image_keys.
   No collection of keys can help the spy get new private keys.*)
 Goal "evs : tls                                      \
-\     ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
+\     ==> ALL KK. (Key(priK B) : analz (Key`KK Un (spies evs))) = \
 \         (priK B : KK | B : bad)";
 by (etac tls.induct 1);
 by (ALLGOALS
@@ -357,13 +357,13 @@
 val analz_image_keys_lemma = result();
 
 (** Strangely, the following version doesn't work:
-\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
+\ ALL Z. (Nonce N : analz (Key`(sessionK`Z) Un (spies evs))) = \
 \        (Nonce N : analz (spies evs))";
 **)
 
 Goal "evs : tls ==>                                    \
 \ ALL KK. KK <= range sessionK -->                     \
-\         (Nonce N : analz (Key``KK Un (spies evs))) = \
+\         (Nonce N : analz (Key`KK Un (spies evs))) = \
 \         (Nonce N : analz (spies evs))";
 by (etac tls.induct 1);
 by (ClientKeyExch_tac 7);
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -147,7 +147,7 @@
 
 Goal "evs : yahalom ==>                              \
 \  ALL K KK. KK <= - (range shrK) -->                \
-\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
+\         (Key K : analz (Key`KK Un (knows Spy evs))) = \
 \         (K : KK | Key K : analz (knows Spy evs))";
 by (etac yahalom.induct 1);
 by analz_knows_Spy_tac;
@@ -367,7 +367,7 @@
 Goal "evs : yahalom ==>                                      \
 \     (ALL KK. KK <= - (range shrK) -->                      \
 \          (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
-\          (Nonce NB : analz (Key``KK Un (knows Spy evs))) =     \
+\          (Nonce NB : analz (Key`KK Un (knows Spy evs))) =     \
 \          (Nonce NB : analz (knows Spy evs)))";
 by (etac yahalom.induct 1);
 by analz_knows_Spy_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -149,7 +149,7 @@
 
 Goal "evs : yahalom ==>                               \
 \  ALL K KK. KK <= - (range shrK) -->                 \
-\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
 \         (K : KK | Key K : analz (knows Spy evs))";
 by (etac yahalom.induct 1);
 by analz_knows_Spy_tac;
diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Yahalom_Bad.ML
--- a/src/HOL/Auth/Yahalom_Bad.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -122,7 +122,7 @@
 
 Goal "evs : yahalom ==>                              \
 \  ALL K KK. KK <= - (range shrK) -->                \
-\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
+\         (Key K : analz (Key`KK Un (knows Spy evs))) = \
 \         (K : KK | Key K : analz (knows Spy evs))";
 by (etac yahalom.induct 1);
 by analz_knows_Spy_tac;