diff -r fe732e890d87 -r f4fa6540e280 ProgTutorial/Tactical.thy --- 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"}.