--- 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}: