CookBook/Tactical.thy
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