doc-src/TutorialI/Rules/rules.tex

 the third unchanged.  With this instantiation, backtracking is neither necessary
 nor possible.
 
 An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
 modified using~\isa{of}, described in
-{\S}\ref{sec:forward} below.   An advantage of \isa{rule_tac} is that the
-instantiations may refer to 
+{\S}\ref{sec:forward} below.   But \isa{rule_tac}, unlike \isa{of}, can 
+express instantiations that refer to 
 \isasymAnd-bound variables in the current subgoal.%
 \index{substitution|)}
 
 
 \section{Quantifiers}

 
 \index{descriptions!definite}%
 A definite description is traditionally written $\iota x.  P(x)$.  It denotes
 the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$;
 otherwise, it returns an arbitrary value of the expected type.
-Isabelle uses \sdx{THE} for the Greek letter~$\iota$.  (The
-traditional notation could be provided, but it is not legible on screen.)
+Isabelle uses \sdx{THE} for the Greek letter~$\iota$.  
+
+%(The traditional notation could be provided, but it is not legible on screen.)
 
 We reason using this rule, where \isa{a} is the unique solution:
 \begin{isabelle}
 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
 \isasymLongrightarrow \ (THE\ x.\ P\ x)\ =\ a%

 \isa{assumption}.  Therefore, we combine these methods using the choice
 operator.
 
 A postfixed question mark~(\isa?)\index{*"? (tactical)} expresses zero or one
 repetitions of a method.  It can also be viewed as the choice between executing a
-method and doing nothing.  It is useless at top level but may be valuable within
-other control structures.%
+method and doing nothing.  It is useless at top level but can be valuable
+within other control structures; for example, 
+\isa{($m$+)?} performs zero or more repetitions of method~$m$.%
 \index{tacticals|)}
 
 
 \subsection{Subgoal Numbering}