--- a/doc-src/TutorialI/Protocol/Public.thy Thu Nov 08 13:23:36 2007 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy Thu Nov 08 13:23:47 2007 +0100
@@ -14,15 +14,14 @@
text {*
The function
@{text pubK} maps agents to their public keys. The function
-@{text priK} maps agents to their private keys. It is defined in terms of
-@{text invKey} and @{text pubK} by a translation; therefore @{text priK} is
-not a proper constant, so we declare it using \isacommand{syntax}
-(cf.\ \S\ref{sec:syntax-translations}).
+@{text priK} maps agents to their private keys. It is merely
+an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
+@{text invKey} and @{text pubK}.
*}
-consts pubK :: "agent => key"
-syntax priK :: "agent => key"
-translations "priK x" \<rightleftharpoons> "invKey(pubK x)"
+consts pubK :: "agent \<Rightarrow> key"
+abbreviation priK :: "agent \<Rightarrow> key"
+where "priK x \<equiv> invKey(pubK x)"
(*<*)
primrec
(*Agents know their private key and all public keys*)
@@ -46,7 +45,7 @@
axioms
inj_pubK: "inj pubK"
- priK_neq_pubK: "priK A ~= pubK B"
+ priK_neq_pubK: "priK A \<noteq> pubK B"
(*<*)
lemmas [iff] = inj_pubK [THEN inj_eq]
@@ -64,7 +63,7 @@
lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
by (simp add: symKeys_def)
-lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
+lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) \<Longrightarrow> K \<noteq> K'"
by blast
lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]