--- a/ProgTutorial/Tactical.thy	Wed Jun 02 08:54:50 2010 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Jun 02 10:08:16 2010 +0200
@@ -68,6 +68,8 @@
   erule}, @{text rule} and @{text assumption}, respectively. The combinator
   @{ML THEN} strings the tactics together.
 
+  TBD: Write something about @{ML_ind prove_multi in Goal}.
+
   \begin{readmore}
   To learn more about the function @{ML_ind prove in Goal} see
   \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file