fix

--- a/doc-src/TutorialI/Protocol/Message.thy	Thu Nov 08 13:23:36 2007 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy	Thu Nov 08 13:23:47 2007 +0100
@@ -34,7 +34,7 @@
 *}
 
 types key = nat
-consts invKey :: "key=>key"
+consts invKey :: "key \<Rightarrow> key"
 (*<*)
 consts all_symmetric :: bool        --{*true if all keys are symmetric*}
 

--- 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 |]

--- a/doc-src/TutorialI/Sets/sets.tex	Thu Nov 08 13:23:36 2007 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Thu Nov 08 13:23:47 2007 +0100
@@ -322,17 +322,13 @@
 \rulenamedx{UN_E}
 \end{isabelle}
 %
-The following built-in syntax translation (see {\S}\ref{sec:syntax-translations})
+The following built-in abbreviation (see {\S}\ref{sec:abbreviations})
 lets us express the union over a \emph{type}:
 \begin{isabelle}
 \ \ \ \ \
-({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
+({\isasymUnion}x.\ B\ x)\ {\isasymequiv}\
 ({\isasymUnion}x{\isasymin}UNIV. B\ x)
 \end{isabelle}
-%Abbreviations work as you might expect.  The term on the left-hand side of
-%the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
-%term is parsed, the reverse translation being done when the term is
-%displayed.
 
 We may also express the union of a set of sets, written \isa{Union\ C} in
 \textsc{ascii}: