--- a/doc-src/TutorialI/Rules/rules.tex Tue Mar 22 16:31:51 2005 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Tue Mar 22 16:32:25 2005 +0100
@@ -2430,7 +2430,7 @@
Explain the use of \isa? and \isa+ in this proof.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
-\isacommand{by}\ (drule\ mp,\ intro?,\ assumption+)+
+\isacommand{by}\ (drule\ mp,\ (intro conjI)?,\ assumption+)+
\end{isabelle}
\end{exercise}