equal
deleted
inserted
replaced
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. |
150 |
150 |
151 Given a subgoal of the form |
151 Given a subgoal of the form |