diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -148,9 +148,9 @@
 \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \medskip
-How does one come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what \isa{auto} leaves unproved. This has
-to provide the clue.  The necessity of universal quantification
+How do we come up with the required lemmas? Try to prove the main theorems
+without them and study carefully what \isa{auto} leaves unproved. This 
+can provide the clue.  The necessity of universal quantification
 (\isa{{\isasymforall}t\ e}) in the two lemmas is explained in
 \S\ref{sec:InductionHeuristics}