summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/IsarImplementation/Thy/Tactic.thy

changeset 46278 | 408e3acfdbb9 |

parent 46277 | aea65ff733b4 |

--- 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