--- 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()
--- 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;
--- 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;
--- 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
--- 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. **)
--- 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;
--- 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;
--- 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;
--- 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;
--- 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";
--- 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
--- 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)";
--- 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";
--- 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
--- 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);
--- 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;
--- 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;
--- 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;