summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 06 Jul 2000 11:23:39 +0200 | |

changeset 9258 | 2121ff73a37d |

parent 9257 | ea5b59af6b31 |

child 9259 | 103acc345f75 |

fixed typos reported by Jeremy Dawson

doc-src/HOL/HOL.tex | file | annotate | diff | comparison | revisions | |

doc-src/Ref/thm.tex | file | annotate | diff | comparison | revisions |

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