--- 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$.
--- 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}