auto update
authorpaulson
Tue Mar 22 16:32:25 2005 +0100 (2005-03-22 ago)
changeset 156174c7bba41483a
parent 15616 cdf6eeb4ac27
child 15618 05bad476e0f0
auto update
doc-src/TutorialI/Rules/rules.tex
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Tue Mar 22 16:31:51 2005 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Tue Mar 22 16:32:25 2005 +0100
     1.3 @@ -2430,7 +2430,7 @@
     1.4  Explain the use of \isa? and \isa+ in this proof.
     1.5  \begin{isabelle}
     1.6  \isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
     1.7 -\isacommand{by}\ (drule\ mp,\ intro?,\ assumption+)+
     1.8 +\isacommand{by}\ (drule\ mp,\ (intro conjI)?,\ assumption+)+
     1.9  \end{isabelle}
    1.10  \end{exercise}
    1.11