doc-src/IsarImplementation/Thy/Tactic.thy
 changeset 46278 408e3acfdbb9 parent 46277 aea65ff733b4
equal inserted replaced
46277:aea65ff733b4 46278:408e3acfdbb9
   280   rules.  The tactic resolves a rule's conclusion with subgoal @{text
   280   rules.  The tactic resolves a rule's conclusion with subgoal @{text
   281   i}, replacing it by the corresponding versions of the rule's
   281   i}, replacing it by the corresponding versions of the rule's
   282   premises.
   282   premises.
   283
   283
   284   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
   284   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
   285   with the given theorems, which should normally be elimination rules.
   285   with the given theorems, which are normally be elimination rules.

   286

   287   Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML

   288   assume_tac}, which facilitates mixing of assumption steps with

   289   genuine eliminations.
   286
   290
   287   \item @{ML dresolve_tac}~@{text "thms i"} performs
   291   \item @{ML dresolve_tac}~@{text "thms i"} performs
   288   destruct-resolution with the given theorems, which should normally
   292   destruct-resolution with the given theorems, which should normally
   289   be destruction rules.  This replaces an assumption by the result of
   293   be destruction rules.  This replaces an assumption by the result of
   290   applying one of the rules.
   294   applying one of the rules.