# HG changeset patch
# User nipkow
# Date 975317923 -3600
# Node ID ed3964d1f1a4fd97ff98e5be664bd34b6b76ae0e
# Parent  06206298e4d034fbec28da165e3cc8352a1c6672
*** empty log message ***

diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Mon Nov 27 10:38:43 2000 +0100
@@ -51,7 +51,7 @@
 
 text{*
 Lexicographic products of measure functions already go a long
-way. Furthermore you may embedding some type in an
+way. Furthermore you may embed some type in an
 existing well-founded relation via the inverse image construction @{term
 inv_image}. All these constructions are known to \isacommand{recdef}. Thus you
 will never have to prove well-foundedness of any relation composed
diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/Advanced/advanced.tex
--- a/doc-src/TutorialI/Advanced/advanced.tex	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/Advanced/advanced.tex	Mon Nov 27 10:38:43 2000 +0100
@@ -35,7 +35,7 @@
 \index{*recdef|)}
 
 \subsection{Beyond measure}
-\label{sec:wellfounded}
+\label{sec:beyond-measure}
 \input{Advanced/document/WFrec.tex}
 
 \section{Advanced induction techniques}
diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Nov 27 10:38:43 2000 +0100
@@ -51,7 +51,7 @@
 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Lexicographic products of measure functions already go a long
-way. Furthermore you may embedding some type in an
+way. Furthermore you may embed some type in an
 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
 will never have to prove well-foundedness of any relation composed
 solely of these building blocks. But of course the proof of
diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Nov 27 10:38:43 2000 +0100
@@ -13,7 +13,7 @@
 the same function. What is more, those equations are automatically declared as
 simplification rules.
 
-In general, Isabelle may not be able to prove all termination condition
+In general, Isabelle may not be able to prove all termination conditions
 (there is one for each recursive call) automatically. For example,
 termination of the following artificial function%
 \end{isamarkuptext}%
diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy	Mon Nov 27 10:38:43 2000 +0100
@@ -13,7 +13,7 @@
 the same function. What is more, those equations are automatically declared as
 simplification rules.
 
-In general, Isabelle may not be able to prove all termination condition
+In general, Isabelle may not be able to prove all termination conditions
 (there is one for each recursive call) automatically. For example,
 termination of the following artificial function
 *}
diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Nov 27 10:38:43 2000 +0100
@@ -549,7 +549,8 @@
 defined by means of \isacommand{recdef}: 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 (user
-supplied) sense.
+supplied) sense. In this section we ristrict ourselves to measure functions;
+more advanced termination proofs are discussed in \S\ref{sec:beyond-measure}.
 
 \subsection{Defining recursive functions}
 
diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Sun Nov 26 11:37:49 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Mon Nov 27 10:38:43 2000 +0100
@@ -1,6 +1,6 @@
 \documentclass{article}
 \newif\ifremarks
-\remarksfalse          %TRUE causes remarks to be displayed (as marginal notes)
+\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
 \usepackage{cl2emono-modified,isabelle,isabellesym}
 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
 \usepackage{proof,amsmath}