Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorChristian Urban <urbanc@in.tum.de>
Wed, 02 Jun 2010 10:08:16 +0200
changeset 437 e2b351efd6f3
parent 436 373f99b1221a
child 438 d9a223c023f6
tuned
ProgTutorial/Tactical.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- 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
Binary file progtutorial.pdf has changed
isabelle-cookbook