--- a/doc-src/AxClass/axclass.tex Mon Feb 01 10:29:11 1999 +0100
+++ b/doc-src/AxClass/axclass.tex Wed Feb 03 13:23:24 1999 +0100
@@ -509,7 +509,7 @@
(see \cite[page 79]{Wenzel94} for more details).
On the other hand there are syntactic differences, of course.
-Constants $\TIMES^\tau$ are rejected by the type checker, unless $\tau
+Constants $\TIMES^\tau$ are rejected by the type-checker, unless $\tau
:: \TT{product}$ is part of the type signature. In our example, this
arity may be always added when required by means of a trivial
\TT{instance}.
@@ -549,7 +549,7 @@
\medskip
While \Isa\ type classes and those of \Haskell\ are almost the same as
-far as type checking and type inference are concerned, there are major
+far as type-checking and type inference are concerned, there are major
semantic differences. \Haskell\ classes require their instances to
\E{provide operations} of certain \E{names}. Therefore, its
\TT{instance} has a \TT{where} part that tells the system what these
--- a/doc-src/Intro/foundations.tex Mon Feb 01 10:29:11 1999 +0100
+++ b/doc-src/Intro/foundations.tex Wed Feb 03 13:23:24 1999 +0100
@@ -431,7 +431,7 @@
\subsection{Signatures and theories}
\index{signatures|bold}
-A {\bf signature} contains the information necessary for type checking,
+A {\bf signature} contains the information necessary for type-checking,
parsing and pretty printing a term. It specifies type classes and their
relationships, types and their arities, constants and their types, etc. It
also contains grammar rules, specified using mixfix declarations.
--- a/doc-src/Logics/CTT.tex Mon Feb 01 10:29:11 1999 +0100
+++ b/doc-src/Logics/CTT.tex Wed Feb 03 13:23:24 1999 +0100
@@ -541,7 +541,7 @@
uses $thms$ with the long introduction and elimination rules to solve goals
of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving
the long rules for defined constants such as the arithmetic operators. The
-tactic can also perform type checking.
+tactic can also perform type-checking.
\item[\ttindexbold{intr_tac} $thms$]
uses $thms$ with the introduction rules to break down a type. It is
@@ -607,7 +607,7 @@
\end{ttbox}
These are loosely based on the intuitionistic proof procedures
of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for
-propositional reasoning may be unsafe for type checking; thus, some of the
+propositional reasoning may be unsafe for type-checking; thus, some of the
`safe' tactics are misnamed.
\begin{ttdescription}
\item[\ttindexbold{mp_tac} $i$]
@@ -729,7 +729,7 @@
This directory contains examples and experimental proofs in {\CTT}.
\begin{ttdescription}
\item[CTT/ex/typechk.ML]
-contains simple examples of type checking and type deduction.
+contains simple examples of type-checking and type deduction.
\item[CTT/ex/elim.ML]
contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
@@ -1071,7 +1071,7 @@
But a completely formal proof is hard to find. The rules can be applied in
countless ways, yielding many higher-order unifiers. The proof can get
bogged down in the details. But with a careful selection of derived rules
-(recall Fig.\ts\ref{ctt-derived}) and the type checking tactics, we can
+(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
prove the theorem in nine steps.
\begin{ttbox}
val prems = Goal
@@ -1092,7 +1092,7 @@
{\out : thm list}
\end{ttbox}
First, \ttindex{intr_tac} applies introduction rules and performs routine
-type checking. This instantiates~$\Var{a}$ to a construction involving
+type-checking. This instantiates~$\Var{a}$ to a construction involving
a $\lambda$-abstraction and an ordered pair. The pair's components are
themselves $\lambda$-abstractions and there is a subgoal for each.
\begin{ttbox}
@@ -1209,7 +1209,7 @@
{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
{\out ?b8(h,x) : C(x,fst(h ` x))}
\end{ttbox}
-Routine type checking goals proliferate in Constructive Type Theory, but
+Routine type-checking goals proliferate in Constructive Type Theory, but
\ttindex{typechk_tac} quickly solves them. Note the inclusion of
\tdx{SumE_fst} along with the premises.
\begin{ttbox}
@@ -1237,7 +1237,7 @@
{\out 3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
\end{ttbox}
The proof object has reached its final form. We call \ttindex{typechk_tac}
-to finish the type checking.
+to finish the type-checking.
\begin{ttbox}
by (typechk_tac prems);
{\out Level 9}
--- a/doc-src/Logics/HOL.tex Mon Feb 01 10:29:11 1999 +0100
+++ b/doc-src/Logics/HOL.tex Wed Feb 03 13:23:24 1999 +0100
@@ -28,7 +28,7 @@
\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
identifies object-level types with meta-level types, taking advantage of
-Isabelle's built-in type checker. It identifies object-level functions
+Isabelle's built-in type-checker. It identifies object-level functions
with meta-level functions, so it uses Isabelle's operations for abstraction
and application.
@@ -562,7 +562,7 @@
\begin{itemize}
\item
Sets are given by predicates over some type~$\sigma$. Types serve to
-define universes for sets, but type checking is still significant.
+define universes for sets, but type-checking is still significant.
\item
There is a universal set (for each type). Thus, sets have complements, and
may be defined by absolute comprehension.
--- a/doc-src/Ref/classical.tex Mon Feb 01 10:29:11 1999 +0100
+++ b/doc-src/Ref/classical.tex Wed Feb 03 13:23:24 1999 +0100
@@ -773,7 +773,7 @@
search. It should estimate the size of the remaining subgoals. A good
heuristic function is \ttindex{size_of_thm}, which measures the size of the
proof state. Another size function might ignore certain subgoals (say,
-those concerned with type checking). A heuristic function might simply
+those concerned with type-checking). A heuristic function might simply
count the subgoals.
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
--- a/doc-src/Ref/goals.tex Mon Feb 01 10:29:11 1999 +0100
+++ b/doc-src/Ref/goals.tex Wed Feb 03 13:23:24 1999 +0100
@@ -622,7 +622,7 @@
\begin{ttdescription}
\item[\ttindexbold{read} {\it string}]
-reads the {\it string} as a term, without type checking.
+reads the {\it string} as a term, without type-checking.
\item[\ttindexbold{prin} {\it t};]
prints the term~$t$ at the terminal.