# HG changeset patch
# User nipkow
# Date 1041585864 -3600
# Node ID 8060978feaf47bb896b98de7d55405df97e904eb
# Parent  a9f000d3ecae411ddb8cfcea91d118e644ca506b
*** empty log message ***

diff -r a9f000d3ecae -r 8060978feaf4 doc-src/TutorialI/IsarOverview/Isar/Induction.thy
--- 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)
diff -r a9f000d3ecae -r 8060978feaf4 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- 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"
diff -r a9f000d3ecae -r 8060978feaf4 doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- 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