--- a/doc-src/TutorialI/Advanced/WFrec.thy Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri May 18 16:45:55 2001 +0200
@@ -37,7 +37,7 @@
example, @{term"measure f"} is always well-founded, and the lexicographic
product of two well-founded relations is again well-founded, which we relied
on when defining Ackermann's function above.
-Of course the lexicographic product can also be interated:
+Of course the lexicographic product can also be iterated:
*}
consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri May 18 16:45:55 2001 +0200
@@ -39,7 +39,7 @@
example, \isa{measure\ f} is always well-founded, and the lexicographic
product of two well-founded relations is again well-founded, which we relied
on when defining Ackermann's function above.
-Of course the lexicographic product can also be interated:%
+Of course the lexicographic product can also be iterated:%
\end{isamarkuptext}%
\isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ contrived\isanewline
--- a/doc-src/TutorialI/Inductive/AB.thy Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Fri May 18 16:45:55 2001 +0200
@@ -102,8 +102,9 @@
intermediate value theorem @{thm[source]nat0_intermed_int_val}
@{thm[display]nat0_intermed_int_val[no_vars]}
where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
-@{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
-integer 1 (see \S\ref{sec:numbers}).
+@{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
+Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
+syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}).
First we show that our specific function, the difference between the
numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
--- a/doc-src/TutorialI/Inductive/Star.thy Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy Fri May 18 16:45:55 2001 +0200
@@ -36,7 +36,7 @@
the standard definition. We start with a simple lemma:
*}
-lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
+lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
by(blast intro: rtc_step);
text{*\noindent
--- a/doc-src/TutorialI/Inductive/document/AB.tex Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri May 18 16:45:55 2001 +0200
@@ -98,8 +98,9 @@
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
\end{isabelle}
where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
-\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
-integer 1 (see \S\ref{sec:numbers}).
+\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
+Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
+syntax.}, and \isa{{\isacharhash}{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
First we show that our specific function, the difference between the
numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
--- a/doc-src/TutorialI/Inductive/document/Star.tex Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri May 18 16:45:55 2001 +0200
@@ -38,7 +38,7 @@
The rest of this section is devoted to proving that it is equivalent to
the standard definition. We start with a simple lemma:%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
--- a/doc-src/TutorialI/Types/Typedef.thy Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Types/Typedef.thy Fri May 18 16:45:55 2001 +0200
@@ -200,7 +200,7 @@
@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
representation: *}
-lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow> Q n";
+lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n \<in> three \<rbrakk> \<Longrightarrow> Q n";
txt{*\noindent
Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
--- a/doc-src/TutorialI/Types/document/Typedef.tex Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Typedef.tex Fri May 18 16:45:55 2001 +0200
@@ -199,7 +199,7 @@
\isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the
representation:%
\end{isamarkuptext}%
-\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharcolon}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}%
+\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated