--- a/doc-src/TutorialI/CTL/CTLind.thy Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy Thu Dec 13 19:05:10 2001 +0100
@@ -31,10 +31,10 @@
text{*
It is easy to see that for any infinite @{term A}-avoiding path @{term f}
-with @{prop"f 0 \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
+with @{prop"f(0::nat) \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
starting with @{term s} because (by definition of @{term Avoid}) there is a
-finite @{term A}-avoiding path from @{term s} to @{term"f 0"}.
-The proof is by induction on @{prop"f 0 \<in> Avoid s A"}. However,
+finite @{term A}-avoiding path from @{term s} to @{term"f(0::nat)"}.
+The proof is by induction on @{prop"f(0::nat) \<in> Avoid s A"}. However,
this requires the following
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
the @{text rule_format} directive undoes the reformulation after the proof.
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Thu Dec 13 19:05:10 2001 +0100
@@ -37,10 +37,10 @@
%
\begin{isamarkuptext}%
It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
-with \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
+with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
starting with \isa{s} because (by definition of \isa{Avoid}) there is a
-finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}.
-The proof is by induction on \isa{f\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymin}\ Avoid\ s\ A}. However,
+finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
+The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
this requires the following
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Dec 13 19:05:10 2001 +0100
@@ -70,18 +70,7 @@
which can yield a fairly complex conclusion. However, @{text rule_format}
can remove any number of occurrences of @{text"\<forall>"} and
@{text"\<longrightarrow>"}.
-*}
-(*<*)
-by auto;
-(*>*)
-(*
-Here is a simple example (which is proved by @{text"blast"}):
-lemma simple[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
-by blast;
-*)
-
-text{*
\index{induction!on a term}%
A second reason why your proposition may not be amenable to induction is that
you want to induct on a complex term, rather than a variable. In
@@ -122,6 +111,7 @@
single theorem because it depends on the number of free variables in $t$ ---
the notation $\overline{y}$ is merely an informal device.
*}
+(*<*)by auto(*>*)
subsection{*Beyond Structural and Recursion Induction*};
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Dec 13 19:05:10 2001 +0100
@@ -81,12 +81,8 @@
Additionally, you may also have to universally quantify some other variables,
which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format}
can remove any number of occurrences of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}}.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isamarkupfalse%
-%
-\begin{isamarkuptext}%
+\isa{{\isasymlongrightarrow}}.
+
\index{induction!on a term}%
A second reason why your proposition may not be amenable to induction is that
you want to induct on a complex term, rather than a variable. In
@@ -126,8 +122,9 @@
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}%
+\end{isamarkuptxt}%
\isamarkuptrue%
+\isamarkupfalse%
%
\isamarkupsubsection{Beyond Structural and Recursion Induction%
}
--- a/doc-src/TutorialI/isabellesym.sty Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/isabellesym.sty Thu Dec 13 19:05:10 2001 +0100
@@ -345,10 +345,10 @@
\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
\newcommand{\isasymwp}{\isamath{\wp}}
\newcommand{\isasymwrong}{\isamath{\wr}}
-\newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
\newcommand{\isasymdieresis}{\isatext{\"\relax}}
-\newcommand{\isasymstruct}{\isamath{\diamond}}
-\newcommand{\isasymindex}{\isamath{\i}}
\newcommand{\isasymcedilla}{\isatext{\c\relax}}
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}
--- a/doc-src/TutorialI/todo.tobias Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Thu Dec 13 19:05:10 2001 +0100
@@ -1,5 +1,3 @@
-"You know my methods. Apply them!"
-
Implementation
==============