changeset 12535 | 626eaec7b5ad |
parent 12489 | c92e38c3cbaa |
child 12540 | a5604ff1ef4e |
--- a/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 14:20:38 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 14:27:57 2001 +0100 @@ -424,7 +424,7 @@ \begin{warn} The term \isa{finite\ A} is defined via a syntax translation as an -abbreviation for \isa{A \isasymin Finites}, where the constant +abbreviation for \isa{A {\isasymin} Finites}, where the constant \cdx{Finites} denotes the set of all finite sets of a given type. There is no constant \isa{finite}. \end{warn}