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,