# HG changeset patch
# User nipkow
# Date 1213274775 -7200
# Node ID 6477705ae3ade16781e4c06aa2626dd261281432
# Parent  65bb0ddb0b9f67056072284841e59e6990f18064
tuned

diff -r 65bb0ddb0b9f -r 6477705ae3ad doc-src/IsarOverview/Isar/Logic.thy
--- 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 -
diff -r 65bb0ddb0b9f -r 6477705ae3ad doc-src/IsarOverview/Isar/document/Induction.tex
--- 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.
diff -r 65bb0ddb0b9f -r 6477705ae3ad doc-src/IsarOverview/Isar/document/Logic.tex
--- 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%