# HG changeset patch
# User paulson
# Date 975424911 -3600
# Node ID f3a17e35d976277aa257d17097c0800d8f8f0e26
# Parent  909c473542f9b10c3c9ad878eb2aaa270242ab8f
added a reference to {sec:products} for ordered pair reasoning

diff -r 909c473542f9 -r f3a17e35d976 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Tue Nov 28 01:48:07 2000 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Tue Nov 28 16:21:51 2000 +0100
@@ -841,13 +841,11 @@
 \isacommand{done}
 \end{isabelle}
 
-Note one detail. The {\isa{auto}} method can prove this but
-{\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,
-allowing the lemmas  to be applied.  A toy example demonstrates this
-point:
+Note one detail. The {\isa{auto}} method can prove this theorem, but
+{\isa{blast}} cannot. 
+The lemmas we have proved apply only to ordered pairs, but {\isa{Auto}}
+replaces a bound variable of product type by a pair of bound variables,
+allowing the lemmas  to be applied.  A toy example demonstrates this point:
 \begin{isabelle}
 \isacommand{lemma}\ "A\ \isasymsubseteq\ Id"\isanewline
 \isacommand{apply}\ (rule\ subsetI)\isanewline
@@ -861,15 +859,15 @@
 \end{isabelle}
 The \isa{simp} and \isa{blast} methods can do nothing here.  However,
 \isa{x} is of product type and therefore denotes an ordered pair.  The
-\isa{auto} method (and some others, including \isa{clarify})
-can replace
+\isa{auto} method (and some others, including \isa{clarify}) replace
 \isa{x} by a pair, which then allows the further simplification from
 \isa{(a,b)\ \isasymin\ A} to \isa{a\ =\ b}.
 \begin{isabelle}
 A\ \isasymsubseteq\ Id\isanewline
 \ 1.\ {\isasymAnd}a\ b.\ (a,b)\ \isasymin\ A\ \isasymLongrightarrow\ a\ =\ b
 \end{isabelle}
-
+Section~\ref{sec:products} will discuss proof techniques for ordered pairs
+in more detail.
 
 
 \section{Well-founded relations and induction}