--- a/doc-src/TutorialI/Sets/sets.tex Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Tue Mar 13 18:35:48 2001 +0100
@@ -323,18 +323,17 @@
\rulename{UN_E}
\end{isabelle}
%
-The following built-in abbreviation lets us express the union
-over a \emph{type}:
+The following built-in syntax translation (see \S\ref{sec:def-translations})
+lets us express the union over a \emph{type}:
\begin{isabelle}
\ \ \ \ \
({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
\end{isabelle}
-Abbreviations work as you might expect. The term on the left-hand side of
-the
-\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
-term is parsed, the reverse translation being done when the term is
-displayed.
+%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}:
@@ -426,10 +425,10 @@
$\binom{n}{k}$.
\begin{warn}
-The term \isa{Finite\ A} is an abbreviation for
-\isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the
-set of all finite sets of a given type. There is no constant
-\isa{Finite}.
+The term \isa{finite\ A} is defined via a syntax translation as an
+abbreviation for \isa{A \isasymin Finites}, where the constant \isa{Finites}
+denotes the set of all finite sets of a given type. There is no constant
+\isa{finite}.
\end{warn}
\index{sets|)}
@@ -1077,4 +1076,4 @@
two agents in a process algebra is an example of coinduction.
The coinduction rule can be strengthened in various ways; see
theory \isa{Gfp} for details.
-\index{fixed points|)}
\ No newline at end of file
+\index{fixed points|)}