doc-src/Logics/CTT.tex
 changeset 975 6c280d1dac35 parent 333 2ca08f62df33 child 3096 ccc2c92bb232
--- a/doc-src/Logics/CTT.tex	Mon Mar 27 18:29:23 1995 +0200
+++ b/doc-src/Logics/CTT.tex	Tue Mar 28 10:24:45 1995 +0200
@@ -533,8 +533,8 @@
\item[\ttindexbold{typechk_tac} $thms$]
uses $thms$ with formation, introduction, and elimination rules to check
the typing of constructions.  It is designed to solve goals of the form
-$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible.  Thus it
-performs Hindley-Milner type inference.  The tactic can also solve goals of
+$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
+performs type inference.  The tactic can also solve goals of
the form $A\;\rm type$.

\item[\ttindexbold{equal_tac} $thms$]