--- a/ProgTutorial/Tactical.thy	Wed Aug 05 16:00:01 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Thu Aug 13 21:32:10 2009 +0200
@@ -1059,6 +1059,8 @@
   will solve all trivial subgoals involving @{term True} or @{term "False"}.
 
   (FIXME: say something about @{ML [index] COND} and COND')
+
+  (FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
   
   \begin{readmore}
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.