
diff -r cdb451206ef9 -r e37e123738f7 doc-src/TutorialI/Sets/sets.tex
--- 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,




