--- a/doc-src/TutorialI/Sets/sets.tex Mon Nov 06 16:43:01 2000 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Mon Nov 06 18:28:22 2000 +0100
@@ -841,7 +841,7 @@
\end{isabelle}
Note one detail. The {\isa{auto}} method can prove this but
-{\isa{blast}} cannot. \remark{move to a later section?}
+{\isa{blast}} cannot. \REMARK{move to a later section?}
This is because the
lemmas we have proved only apply to ordered pairs. {\isa{Auto}} can
convert a bound variable of a product type into a pair of bound variables,