doc-src/IsarImplementation/Thy/document/Tactic.tex

   using the given theorems, which should normally be introduction
   rules.  The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's
   premises.
 
   \item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution
-  with the given theorems, which should normally be elimination rules.
+  with the given theorems, which are normally be elimination rules.
+
+  Note that \verb|eresolve_tac [asm_rl]| is equivalent to \verb|assume_tac|, which facilitates mixing of assumption steps with
+  genuine eliminations.
 
   \item \verb|dresolve_tac|~\isa{thms\ i} performs
   destruct-resolution with the given theorems, which should normally
   be destruction rules.  This replaces an assumption by the result of
   applying one of the rules.