author nipkow Tue, 20 Feb 2001 10:37:12 +0100 changeset 11159 07b13770c4d6 parent 11158 5652018b809a child 11160 e0ab13bec5c8
*** empty log message ***
 doc-src/TutorialI/Recdef/Induction.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Recdef/document/Induction.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Rules/rules.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Sets/sets.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/appendix.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/fp.tex file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/Recdef/Induction.thy	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Feb 20 10:37:12 2001 +0100
@@ -47,7 +47,7 @@

In general, the format of invoking recursion induction is
\begin{quote}
-\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
+\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
\end{quote}\index{*induct_tac}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Feb 20 10:37:12 2001 +0100
@@ -49,7 +49,7 @@

In general, the format of invoking recursion induction is
\begin{quote}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
+\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
\end{quote}\index{*induct_tac}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
--- a/doc-src/TutorialI/Rules/rules.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Tue Feb 20 10:37:12 2001 +0100
@@ -570,7 +570,7 @@
placeholders for terms.  \emph{Unification} refers to  the process of
making two terms identical, possibly by replacing their schematic variables by
terms.  The simplest case is when the two terms  are already the same. Next
-simplest is when the variables in only one of the term
+simplest is when the variables in only one of the terms
are replaced; this is called pattern-matching.  The
\isa{rule} method typically  matches the rule's conclusion
against the current subgoal.  In the most complex case,  variables in both
@@ -655,7 +655,7 @@
resulting subgoal is trivial by assumption, so the \isacommand{by} command
proves it implicitly.

-We are using the \isa{erule} method it in a novel way. Hitherto,
+We are using the \isa{erule} method in a novel way. Hitherto,
the conclusion of the rule was just a variable such as~\isa{?R}, but it may
be any term. The conclusion is unified with the subgoal just as
it would be with the \isa{rule} method. At the same time \isa{erule} looks 
--- a/doc-src/TutorialI/Sets/sets.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Tue Feb 20 10:37:12 2001 +0100
@@ -374,7 +374,7 @@
\isa{Collect},\index{*Collect (constant)}
which occasionally appears when a goal or theorem
is displayed.  For example, \isa{Collect\ P}  is the same term as
-\isa{\isacharbraceleft z.\ P\ x\isacharbraceright}.  The same thing can
+\isa{\isacharbraceleft x.\ P\ x\isacharbraceright}.  The same thing can
happen with quantifiers:   \hbox{\isa{All\ P}}\index{*All (constant)}
is
\isa{{\isasymforall}z.\ P\ x} and 
--- a/doc-src/TutorialI/appendix.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex	Tue Feb 20 10:37:12 2001 +0100
@@ -53,7 +53,7 @@
\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} & \verb$\<exists>!$\\ \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
-\ttindexbold{SOME} &
+\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} & \verb$\<epsilon>$\\ \indexboldpos{\isasymcirc}{$HOL1} &
\ttindexbold{o} &
--- a/doc-src/TutorialI/fp.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Tue Feb 20 10:37:12 2001 +0100
@@ -297,7 +297,7 @@

Simplification is one of the central theorem proving tools in Isabelle and
many other systems. The tool itself is called the \bfindex{simplifier}. The
-purpose of this section is introduce the many features of the simplifier.
+purpose of this section is to introduce the many features of the simplifier.
Anybody intending to perform proofs in HOL should read this section. Later on
({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
little bit of how the simplifier works. The serious student should read that
@@ -466,7 +466,7 @@
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. In this section we ristrict ourselves to measure functions;
+supplied) sense. In this section we restrict ourselves to measure functions;
more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.

\subsection{Defining Recursive Functions}