1.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Thu Nov 08 13:23:36 2007 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Thu Nov 08 13:23:47 2007 +0100
     1.3 @@ -14,15 +14,14 @@
     1.4  text {*
     1.5  The function
     1.6  @{text pubK} maps agents to their public keys.  The function
     1.7 -@{text priK} maps agents to their private keys.  It is defined in terms of
     1.8 -@{text invKey} and @{text pubK} by a translation; therefore @{text priK} is
     1.9 -not a proper constant, so we declare it using \isacommand{syntax}
    1.10 -(cf.\ \S\ref{sec:syntax-translations}).
    1.11 +@{text priK} maps agents to their private keys.  It is merely
    1.12 +an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
    1.13 +@{text invKey} and @{text pubK}.
    1.14  *}
    1.15  
    1.16 -consts pubK :: "agent => key"
    1.17 -syntax priK :: "agent => key"
    1.18 -translations "priK x" \<rightleftharpoons> "invKey(pubK x)"
    1.19 +consts pubK :: "agent \<Rightarrow> key"
    1.20 +abbreviation priK :: "agent \<Rightarrow> key"
    1.21 +where "priK x  \<equiv>  invKey(pubK x)"
    1.22  (*<*)
    1.23  primrec
    1.24          (*Agents know their private key and all public keys*)
    1.25 @@ -46,7 +45,7 @@
    1.26  
    1.27  axioms
    1.28    inj_pubK:        "inj pubK"
    1.29 -  priK_neq_pubK:   "priK A ~= pubK B"
    1.30 +  priK_neq_pubK:   "priK A \<noteq> pubK B"
    1.31  (*<*)
    1.32  lemmas [iff] = inj_pubK [THEN inj_eq]
    1.33  
    1.34 @@ -64,7 +63,7 @@
    1.35  lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
    1.36    by (simp add: symKeys_def)
    1.37  
    1.38 -lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
    1.39 +lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) \<Longrightarrow> K \<noteq> K'"
    1.40    by blast
    1.41  
    1.42  lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]