doc-src/IsarImplementation/Thy/document/Tactic.tex
 changeset 46278 408e3acfdbb9 parent 46277 aea65ff733b4
equal inserted replaced
46277:aea65ff733b4 46278:408e3acfdbb9
   336   using the given theorems, which should normally be introduction
   336   using the given theorems, which should normally be introduction
   337   rules.  The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's
   337   rules.  The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's
   338   premises.
   338   premises.
   339
   339
   340   \item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution
   340   \item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution
   341   with the given theorems, which should normally be elimination rules.
   341   with the given theorems, which are normally be elimination rules.

   342

   343   Note that \verb|eresolve_tac [asm_rl]| is equivalent to \verb|assume_tac|, which facilitates mixing of assumption steps with

   344   genuine eliminations.
   342
   345
   343   \item \verb|dresolve_tac|~\isa{thms\ i} performs
   346   \item \verb|dresolve_tac|~\isa{thms\ i} performs
   344   destruct-resolution with the given theorems, which should normally
   347   destruct-resolution with the given theorems, which should normally
   345   be destruction rules.  This replaces an assumption by the result of
   348   be destruction rules.  This replaces an assumption by the result of
   346   applying one of the rules.
   349   applying one of the rules.