corrected trivial typo;
authorwenzelm
Thu Nov 25 14:16:40 1993 +0100 (1993-11-25)
changeset 14867d046de093e
parent 147 e8d8fa0ddcef
child 149 caa7a52ff46f
corrected trivial typo;
doc-src/Ref/substitution.tex
     1.1 --- a/doc-src/Ref/substitution.tex	Thu Nov 25 13:54:21 1993 +0100
     1.2 +++ b/doc-src/Ref/substitution.tex	Thu Nov 25 14:16:40 1993 +0100
     1.3 @@ -143,7 +143,7 @@
     1.4  \begin{ttbox} 
     1.5  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u);
     1.6  \end{ttbox}
     1.7 -Here {\tt Trueprop} is the coercion from type'~$o$ to type~$prop$, while
     1.8 +Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
     1.9  \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
    1.10  Pattern-matching expresses the function concisely, using wildcards~({\tt_})
    1.11  to hide the types.