doc-src/Ref/substitution.tex
 changeset 286 e7efbf03562b parent 148 67d046de093e child 323 361a71713176
equal inserted replaced
285:fd4a6585e5bf 286:e7efbf03562b
   139 of the object-logic.  It is not concerned with the names of the equality
   139 of the object-logic.  It is not concerned with the names of the equality
   140 and implication symbols, or the types of formula and terms.  Coding the
   140 and implication symbols, or the types of formula and terms.  Coding the
   141 function {\tt dest_eq} requires knowledge of Isabelle's representation of
   141 function {\tt dest_eq} requires knowledge of Isabelle's representation of
   142 terms.  For {\tt FOL} it is defined by
   142 terms.  For {\tt FOL} it is defined by
   143 \begin{ttbox}
   143 \begin{ttbox}
   144 fun dest_eq (Const("Trueprop",_) $(Const("op =",_)$t$u)) = (t,u);  144 fun dest_eq (Const("Trueprop",_)$ (Const("op =",_)$t$u)) = (t,u)
   145 \end{ttbox}
   145 \end{ttbox}
   146 Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
   146 Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
   147 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
   147 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
   148 Pattern-matching expresses the function concisely, using wildcards~({\tt_})
   148 Pattern-matching expresses the function concisely, using wildcards~({\tt_})
   149 to hide the types.
   149 to hide the types.