# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275466096 -7200
# Node ID e2b351efd6f3489f28b3d164ba0085546906676c
# Parent  373f99b1221adaf319986f1141ee02e2a865dbc7
tuned

diff -r 373f99b1221a -r e2b351efd6f3 ProgTutorial/Tactical.thy
--- 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
diff -r 373f99b1221a -r e2b351efd6f3 progtutorial.pdf
Binary file progtutorial.pdf has changed