# HG changeset patch
# User paulson
# Date 918044604 -3600
# Node ID 9a59cf8ae9b5a35d7d396f5fde99d83e4e034677
# Parent  f3f2560fbed94f550721dc7ae714723b363c0973
standard spelling: type-checking

diff -r f3f2560fbed9 -r 9a59cf8ae9b5 doc-src/AxClass/axclass.tex
--- 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
diff -r f3f2560fbed9 -r 9a59cf8ae9b5 doc-src/Intro/foundations.tex
--- 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.
diff -r f3f2560fbed9 -r 9a59cf8ae9b5 doc-src/Logics/CTT.tex
--- 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}
diff -r f3f2560fbed9 -r 9a59cf8ae9b5 doc-src/Logics/HOL.tex
--- 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.
diff -r f3f2560fbed9 -r 9a59cf8ae9b5 doc-src/Ref/classical.tex
--- 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
diff -r f3f2560fbed9 -r 9a59cf8ae9b5 doc-src/Ref/goals.tex
--- 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.