--- 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}