# HG changeset patch
# User paulson
# Date 1111505545 -3600
# Node ID 4c7bba41483afde238b33a2749d4811c0b6d878b
# Parent  cdf6eeb4ac27a776ec05605bc7f37a9ffa494733
auto update

diff -r cdf6eeb4ac27 -r 4c7bba41483a doc-src/TutorialI/Rules/rules.tex
--- 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}