changeset 12649 | 6e17f2ae9e16 |
parent 12540 | a5604ff1ef4e |
child 12815 | 1f073030b97a |
--- a/doc-src/TutorialI/Sets/sets.tex Sun Jan 06 13:48:18 2002 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Sun Jan 06 16:50:31 2002 +0100 @@ -324,7 +324,7 @@ \rulenamedx{UN_E} \end{isabelle} % -The following built-in syntax translation (see {\S}\ref{sec:def-translations}) +The following built-in syntax translation (see {\S}\ref{sec:syntax-translations}) lets us express the union over a \emph{type}: \begin{isabelle} \ \ \ \ \