# HG changeset patch
# User paulson
# Date 962875419 -7200
# Node ID 2121ff73a37d814325ee284e9a3dda832a708d62
# Parent  ea5b59af6b31196c13b8f7157e753865a7d6598f
fixed typos reported by Jeremy Dawson

diff -r ea5b59af6b31 -r 2121ff73a37d doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Thu Jul 06 10:10:50 2000 +0200
+++ b/doc-src/HOL/HOL.tex	Thu Jul 06 11:23:39 2000 +0200
@@ -1997,7 +1997,7 @@
 $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em
   admissible} types containing at most the type variables $\alpha@1, \ldots,
 \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em
-  admissible} iff
+  admissible} if and only if
 \begin{itemize}
 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
 newly defined type constructors $t@1,\ldots,t@n$, or
@@ -2046,7 +2046,7 @@
 \medskip
 
 Types in HOL must be non-empty. Each of the new datatypes
-$(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty iff it has a
+$(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a
 constructor $C^j@i$ with the following property: for all argument types
 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype
 $(\vec{\alpha})t@{j'}$ is non-empty.
@@ -2704,19 +2704,22 @@
   (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.
   
 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
-  relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$.
+  relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if
+  $f(x)<f(y)$.  
   Typically, $f$ takes the recursive function's arguments (as a tuple) and
   returns a result expressed in terms of the function \texttt{size}.  It is
   called a \textbf{measure function}.  Recall that \texttt{size} is overloaded
   and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
                                                     
-\item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
-  \texttt{measure}.  It specifies a relation such that $x\prec y$ iff $f(x)$
+\item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of
+  \texttt{measure}.  It specifies a relation such that $x\prec y$ if and only
+  if $f(x)$ 
   is less than $f(y)$ according to~$R$, which must itself be a well-founded
   relation.
 
 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations.  It
-  is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$
+  is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only
+  if $x@1$ 
   is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$
   is less than $y@2$ according to~$R@2$.
 
diff -r ea5b59af6b31 -r 2121ff73a37d doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Thu Jul 06 10:10:50 2000 +0200
+++ b/doc-src/Ref/thm.tex	Thu Jul 06 11:23:39 2000 +0200
@@ -608,8 +608,9 @@
 $\phi[\Var{x@k}/x]$.  Thus, it replaces the outermost $\Forall$-bound
 variable by an unknown having subscript~$k$.
 
-\item[\ttindexbold{forall_elim_vars} $ks$ $thm$] 
-applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$.
+\item[\ttindexbold{forall_elim_vars} $k$ $thm$] 
+applies {\tt forall_elim_var}~$k$ repeatedly until the theorem no longer has
+the form $\Forall x.\phi$.
 \end{ttdescription}