--- a/doc-src/IsarOverview/Isar/Logic.thy Thu Jun 12 14:33:28 2008 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy Thu Jun 12 14:46:15 2008 +0200
@@ -314,9 +314,10 @@
\end{center}
Sometimes it is necessary to suppress the implicit application of rules in a
-\isakeyword{proof}. For example \isakeyword{show}~@{prop"A \<or> B"} would
-trigger $\lor$-introduction, requiring us to prove @{prop A}. A simple
-``@{text"-"}'' prevents this \emph{faux pas}: *}
+\isakeyword{proof}. For example \isakeyword{show(s)}~@{prop[source]"P \<or> Q"}
+would trigger $\lor$-introduction, requiring us to prove @{prop P}, which may
+not be what we had in mind.
+A simple ``@{text"-"}'' prevents this \emph{faux pas}: *}
lemma assumes AB: "A \<or> B" shows "B \<or> A"
proof -
--- a/doc-src/IsarOverview/Isar/document/Induction.tex Thu Jun 12 14:33:28 2008 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex Thu Jun 12 14:46:15 2008 +0200
@@ -66,11 +66,11 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where
-\isa{case{\isacharunderscore}split{\isacharunderscore}thm} is \isa{{\isasymlbrakk}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}. If we reverse
+\noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharparenright}} where
+\isa{case{\isacharunderscore}split} is \isa{{\isasymlbrakk}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}. If we reverse
the order of the two cases in the proof, the first case would prove
\isa{{\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A} which would solve the first premise of
-\isa{case{\isacharunderscore}split{\isacharunderscore}thm}, instantiating \isa{{\isacharquery}P} with \isa{{\isasymnot}\ A}, thus making the second premise \isa{{\isasymnot}\ {\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A}.
+\isa{case{\isacharunderscore}split}, instantiating \isa{{\isacharquery}P} with \isa{{\isasymnot}\ A}, thus making the second premise \isa{{\isasymnot}\ {\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A}.
Therefore the order of subgoals is not always completely arbitrary.
The above proof is appropriate if \isa{A} is textually small.
--- a/doc-src/IsarOverview/Isar/document/Logic.tex Thu Jun 12 14:33:28 2008 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex Thu Jun 12 14:46:15 2008 +0200
@@ -699,9 +699,10 @@
\end{center}
Sometimes it is necessary to suppress the implicit application of rules in a
-\isakeyword{proof}. For example \isakeyword{show}~\isa{A\ {\isasymor}\ B} would
-trigger $\lor$-introduction, requiring us to prove \isa{A}. A simple
-``\isa{{\isacharminus}}'' prevents this \emph{faux pas}:%
+\isakeyword{proof}. For example \isakeyword{show(s)}~\isa{{\isachardoublequote}P\ {\isasymor}\ Q{\isachardoublequote}}
+would trigger $\lor$-introduction, requiring us to prove \isa{P}, which may
+not be what we had in mind.
+A simple ``\isa{{\isacharminus}}'' prevents this \emph{faux pas}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%