# HG changeset patch
# User nipkow
# Date 982661832 -3600
# Node ID 07b13770c4d69ac5271214c1a51bb8e2e3584824
# Parent  5652018b809a08572531d806d290bf0a353a490e
*** empty log message ***

diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/Recdef/Induction.thy
--- 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
diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/Recdef/document/Induction.tex
--- 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
diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/Rules/rules.tex
--- 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 
diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/Sets/sets.tex
--- 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 
diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/appendix.tex
--- 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} &
diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/fp.tex
--- 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}