changeset 126 | fcc0e6e54dca |
parent 120 | c39f83d8daeb |
child 128 | 693711a0c702 |
--- a/CookBook/Tactical.thy Thu Feb 19 01:09:16 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 19 14:44:53 2009 +0000 @@ -398,8 +398,6 @@ (*<*)oops(*>*) text {* - (FIXME: is it important to get the number of subgoals?) - The function @{ML resolve_tac} is similar to @{ML rtac}, except that it expects a list of theorems as arguments. From this list it will apply the first applicable theorem (later theorems that are also applicable can be