doc-src/Ref/substitution.tex
changeset 148 67d046de093e
parent 104 d8205bb279a7
child 286 e7efbf03562b
--- a/doc-src/Ref/substitution.tex	Thu Nov 25 13:54:21 1993 +0100
+++ b/doc-src/Ref/substitution.tex	Thu Nov 25 14:16:40 1993 +0100
@@ -143,7 +143,7 @@
 \begin{ttbox} 
 fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u);
 \end{ttbox}
-Here {\tt Trueprop} is the coercion from type'~$o$ to type~$prop$, while
+Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
 Pattern-matching expresses the function concisely, using wildcards~({\tt_})
 to hide the types.