# HG changeset patch
# User nipkow
# Date 988797258 -7200
# Node ID 9710486b886b35e3c5385c55b2dfd257976d5f50
# Parent  a2bff98d6e5deb9df97da34a96e7669160f7d1c2
*** empty log message ***

diff -r a2bff98d6e5d -r 9710486b886b doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue May 01 22:26:55 2001 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed May 02 11:54:18 2001 +0200
@@ -111,11 +111,14 @@
 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
 little leads to the goal
-\[ \bigwedge\vec{y}.~\forall \vec{z}.~ t(\vec{z}) \prec t(\vec{y}) \longrightarrow C(\vec{z})
-   \Longrightarrow C(\vec{y}) \]
-where the dependence of $t$ and $C$ on their free variables has been made explicit.
-Unfortunately, this induction schema cannot be expressed as a single theorem because it depends
-on the number of free variables in $t$ --- the notation $\vec{y}$ is merely an informal device.
+\[ \bigwedge\overline{y}.\ 
+   \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
+    \ \Longrightarrow\ C\,\overline{y} \]
+where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
+$C$ on the free variables of $t$ has been made explicit.
+Unfortunately, this induction schema cannot be expressed as a
+single theorem because it depends on the number of free variables in $t$ ---
+the notation $\overline{y}$ is merely an informal device.
 *}
 
 subsection{*Beyond Structural and Recursion Induction*};
@@ -133,7 +136,8 @@
 induction, where you must prove $P(n)$ under the assumption that $P(m)$
 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
 @{thm[display]"nat_less_induct"[no_vars]}
-Here is an example of its application.
+As an example of its application we prove a property of the following
+function:
 *};
 
 consts f :: "nat \<Rightarrow> nat";
diff -r a2bff98d6e5d -r 9710486b886b doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue May 01 22:26:55 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed May 02 11:54:18 2001 +0200
@@ -104,11 +104,14 @@
 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
 little leads to the goal
-\[ \bigwedge\vec{y}.~\forall \vec{z}.~ t(\vec{z}) \prec t(\vec{y}) \longrightarrow C(\vec{z})
-   \Longrightarrow C(\vec{y}) \]
-where the dependence of $t$ and $C$ on their free variables has been made explicit.
-Unfortunately, this induction schema cannot be expressed as a single theorem because it depends
-on the number of free variables in $t$ --- the notation $\vec{y}$ is merely an informal device.%
+\[ \bigwedge\overline{y}.\ 
+   \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
+    \ \Longrightarrow\ C\,\overline{y} \]
+where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
+$C$ on the free variables of $t$ has been made explicit.
+Unfortunately, this induction schema cannot be expressed as a
+single theorem because it depends on the number of free variables in $t$ ---
+the notation $\overline{y}$ is merely an informal device.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Beyond Structural and Recursion Induction%
@@ -130,7 +133,8 @@
 \begin{isabelle}%
 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
 \end{isabelle}
-Here is an example of its application.%
+As an example of its application we prove a property of the following
+function:%
 \end{isamarkuptext}%
 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%