# HG changeset patch
# User paulson
# Date 975947388 -3600
# Node ID b9c290f0343d2c8f7614c42f78a97334e0bcbd16
# Parent  92d3cbea80b2ce77503038032349fdc5b0dd23a4
auto update

diff -r 92d3cbea80b2 -r b9c290f0343d doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Fri Dec 01 20:24:08 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Dec 04 17:29:48 2000 +0100
@@ -25,9 +25,8 @@
 In general, \isacommand{recdef} supports termination proofs based on
 arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
 This is called \textbf{well-founded
-recursion}\indexbold{recursion!well-founded}\index{well-founded
-recursion|see{recursion, well-founded}}. Clearly, a function definition is
-total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+recursion}\indexbold{recursion!well-founded}. Clearly, a function definition
+is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
 left-hand side of an equation and $r$ the argument of some recursive call on
 the corresponding right-hand side, induces a well-founded relation.  For a
 systematic account of termination proofs via well-founded relations see, for
diff -r 92d3cbea80b2 -r b9c290f0343d doc-src/TutorialI/Types/document/Pairs.tex
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Fri Dec 01 20:24:08 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Mon Dec 04 17:29:48 2000 +0100
@@ -154,7 +154,8 @@
 \begin{isamarkuptxt}%
 \noindent
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\ swap\ {\isacharparenleft}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline
+\ \ \ \ \ \ \ swap\ {\isacharparenleft}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}%
 \end{isabelle}%
 \end{isamarkuptxt}%
 \isacommand{apply}\ simp\isanewline