--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Mon Dec 30 18:33:15 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Fri Jan 03 10:24:24 2003 +0100
@@ -8,7 +8,7 @@
and @{text Cons}. @{text Nil} is written @{term"[]"} and @{text"Cons x
xs"} is written @{term"x # xs"}. *}
-subsection{*Case distinction*}
+subsection{*Case distinction\label{sec:CaseDistinction}*}
text{* We have already met the @{text cases} method for performing
binary case splits. Here is another example: *}
@@ -47,7 +47,7 @@
The same game can be played with other datatypes, for example lists,
where @{term tl} is the tail of a list, and @{text length} returns a
-natural number:
+natural number (remember: $0-1=0$):
%\Tweakskip
*}
(*<*)declare length_tl[simp del](*>*)
@@ -286,7 +286,7 @@
equation.
The proof is so simple that it can be condensed to
-%\Tweakskip
+\Tweakskip
*}
(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
by (induct xs rule: rot.induct, simp_all)
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Mon Dec 30 18:33:15 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Fri Jan 03 10:24:24 2003 +0100
@@ -90,7 +90,7 @@
This is too much proof text. Elimination rules should be selected
automatically based on their major premise, the formula or rather connective
-to be eliminated. In Isar they are triggered by propositions being fed
+to be eliminated. In Isar they are triggered by facts being fed
\emph{into} a proof. Syntax:
\begin{center}
\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof}
@@ -114,7 +114,7 @@
qed
qed
-text{* Now we come a second important principle:
+text{* Now we come to a second important principle:
\begin{quote}\em
Try to arrange the sequence of propositions in a UNIX-like pipe,
such that the proof of each proposition builds on the previous proposition.
@@ -266,7 +266,12 @@
\item[\isakeyword{next}] deals with multiple subgoals. For example,
when showing @{term"A \<and> B"} we need to show both @{term A} and @{term
B}. Each subgoal is proved separately, in \emph{any} order. The
-individual proofs are separated by \isakeyword{next}.
+individual proofs are separated by \isakeyword{next}. \footnote{Each
+\isakeyword{show} must prove one of the pending subgoals. If a
+\isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals
+contain ?-variables, the first one is proved. Thus the order in which
+the subgoals are proved can matter --- see
+\S\ref{sec:CaseDistinction} for an example.}
Strictly speaking \isakeyword{next} is only required if the subgoals
are proved in different assumption contexts which need to be
@@ -479,7 +484,7 @@
@{text blast} to achieve bigger proof steps, there may still be the
tendency to use the default introduction and elimination rules to
decompose goals and facts. This can lead to very tedious proofs:
-%\Tweakskip
+\Tweakskip
*}
(*<*)ML"set quick_and_dirty"(*>*)
lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Dec 30 18:33:15 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Fri Jan 03 10:24:24 2003 +0100
@@ -32,7 +32,7 @@
\input{intro.tex}
\input{Logic.tex}
-%\Tweakskip\Tweakskip
+\Tweakskip\Tweakskip
\input{Induction.tex}
%\Tweakskip