doc-src/Ref/tactic.tex
 changeset 46278 408e3acfdbb9 parent 46277 aea65ff733b4 child 46295 2548a85b0e02
equal inserted replaced
46277:aea65ff733b4 46278:408e3acfdbb9
    64   equalities ($\equiv$).  More general equivalences are handled by the
    64   equalities ($\equiv$).  More general equivalences are handled by the
    65   simplifier, provided that it is set up appropriately for your logic
    65   simplifier, provided that it is set up appropriately for your logic
    66   (see Chapter~\ref{chap:simplification}).
    66   (see Chapter~\ref{chap:simplification}).
    67 \end{warn}
    67 \end{warn}
    68
    68
    86
    69
    87 \subsection{Composition: resolution without lifting}
    70 \subsection{Composition: resolution without lifting}
    88 \index{tactics!for composition}
    71 \index{tactics!for composition}
    89 \begin{ttbox}
    72 \begin{ttbox}
    90 compose_tac: (bool * thm * int) -> int -> tactic
    73 compose_tac: (bool * thm * int) -> int -> tactic