# HG changeset patch
# User nipkow
# Date 1194015409 -3600
# Node ID b5474493503639168a2d82f3500c47e6a0dffffe
# Parent  d0928156e326c457822e58c3a39c7cf5223c8f91
*** empty log message ***

diff -r d0928156e326 -r b54744935036 doc-src/TutorialI/Fun/document/fun0.tex
--- a/doc-src/TutorialI/Fun/document/fun0.tex	Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/Fun/document/fun0.tex	Fri Nov 02 15:56:49 2007 +0100
@@ -73,7 +73,7 @@
 \isa{sep{\isadigit{1}}\ a\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}}.  Thus the functions \isa{sep} and
 \isa{sep{\isadigit{1}}} are identical.
 
-Because of its pattern-matching syntax, \isacommand{fun} is also useful
+Because of its pattern matching syntax, \isacommand{fun} is also useful
 for the definition of non-recursive functions:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -116,7 +116,7 @@
 \ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
 \ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}ack{\isadigit{2}}\ n\ {\isacharparenleft}Suc\ m{\isacharparenright}{\isacharparenright}\ m{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-Thus the order of arguments has no influence on whether
+The order of arguments has no influence on whether
 \isacommand{fun} can prove termination of a function. For more details
 see elsewhere~\cite{bulwahnKN07}.
 
@@ -185,8 +185,8 @@
 \begin{isamarkuptext}%
 \noindent
 The order of equations is important: it hides the side condition
-\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}.  Unfortunately, in general the case distinction
-may not be expressible by pattern matching.
+\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}.  Unfortunately, not all conditionals can be
+expressed by pattern matching.
 
 A simple alternative is to replace \isa{if} by \isa{case}, 
 which is also available for \isa{bool} and is not split automatically:%
@@ -316,16 +316,18 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Try proving the above lemma by structural induction, and you find that you
-need an additional case distinction.
+\noindent The proof goes smoothly because the induction rule
+follows the recursion of \isa{sep}.  Try proving the above lemma by
+structural induction, and you find that you need an additional case
+distinction.
 
 In general, the format of invoking recursion induction is
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
 \end{quote}\index{*induct_tac (method)}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$-tuple. Usually the subgoal will
-contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
+name of a function that takes an $n$ arguments. Usually the subgoal will
+contain the term $f x@1 \dots x@n$ but this need not be the case. The
 induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
 \begin{isabelle}
 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
diff -r d0928156e326 -r b54744935036 doc-src/TutorialI/Fun/fun0.thy
--- a/doc-src/TutorialI/Fun/fun0.thy	Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy	Fri Nov 02 15:56:49 2007 +0100
@@ -57,7 +57,7 @@
 @{prop"sep1 a [x] = [x]"}.  Thus the functions @{const sep} and
 @{const sep1} are identical.
 
-Because of its pattern-matching syntax, \isacommand{fun} is also useful
+Because of its pattern matching syntax, \isacommand{fun} is also useful
 for the definition of non-recursive functions:
 *}
 
@@ -98,7 +98,7 @@
   "ack2 0 (Suc m) = ack2 (Suc 0) m" |
   "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
 
-text{* Thus the order of arguments has no influence on whether
+text{* The order of arguments has no influence on whether
 \isacommand{fun} can prove termination of a function. For more details
 see elsewhere~\cite{bulwahnKN07}.
 
@@ -157,8 +157,8 @@
 
 text{*\noindent
 The order of equations is important: it hides the side condition
-@{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
-may not be expressible by pattern matching.
+@{prop"n ~= (0::nat)"}.  Unfortunately, not all conditionals can be
+expressed by pattern matching.
 
 A simple alternative is to replace @{text "if"} by @{text case}, 
 which is also available for @{typ bool} and is not split automatically:
@@ -233,17 +233,18 @@
 apply simp_all;
 done
 
-text{*
-Try proving the above lemma by structural induction, and you find that you
-need an additional case distinction.
+text{*\noindent The proof goes smoothly because the induction rule
+follows the recursion of @{const sep}.  Try proving the above lemma by
+structural induction, and you find that you need an additional case
+distinction.
 
 In general, the format of invoking recursion induction is
 \begin{quote}
 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
 \end{quote}\index{*induct_tac (method)}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$-tuple. Usually the subgoal will
-contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
+name of a function that takes an $n$ arguments. Usually the subgoal will
+contain the term $f x@1 \dots x@n$ but this need not be the case. The
 induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
 \begin{isabelle}
 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
diff -r d0928156e326 -r b54744935036 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/fp.tex	Fri Nov 02 15:56:49 2007 +0100
@@ -133,7 +133,7 @@
 \thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
 The latter contains many further operations. For example, the functions
 \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
-element and the remainder of a list. (However, pattern-matching is usually
+element and the remainder of a list. (However, pattern matching is usually
 preferable to \isa{hd} and \isa{tl}.)  
 Also available are higher-order functions like \isa{map} and \isa{filter}.
 Theory \isa{List} also contains
@@ -465,7 +465,7 @@
 
 Although many total functions have a natural primitive recursive definition,
 this is not always the case. Arbitrary total recursive functions can be
-defined by means of \isacommand{fun}: you can use full pattern-matching,
+defined by means of \isacommand{fun}: you can use full pattern matching,
 recursion need not involve datatypes, and termination is proved by showing
 that the arguments of all recursive calls are smaller in a suitable sense.
 In this section we restrict ourselves to functions where Isabelle can prove