doc-src/IsarImplementation/Thy/Tactic.thy

--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Sun Jan 29 22:00:10 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Sun Jan 29 22:12:25 2012 +0100
@@ -282,7 +282,11 @@
   premises.
 
   \item @{ML eresolve_tac}~@{text "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 @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML
+  assume_tac}, which facilitates mixing of assumption steps with
+  genuine eliminations.
 
   \item @{ML dresolve_tac}~@{text "thms i"} performs
   destruct-resolution with the given theorems, which should normally