# HG changeset patch
# User nipkow
# Date 984417791 -3600
# Node ID f8da11ca4c6e8abe310286ffba571398c405858b
# Parent  eddc69b55facb433a56dbcff99dce3ccefb02f53
*** empty log message ***

diff -r eddc69b55fac -r f8da11ca4c6e doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Mon Mar 12 18:17:45 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Mon Mar 12 18:23:11 2001 +0100
@@ -86,14 +86,10 @@
 literature. In Recdef/termination.thy, at the end.
 %FIXME, with one exception: nested recursion.
 
-Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
+Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
 
 Appendix with list functions.
 
-Move section on rule inversion further to the front, and combine
-\subsection{Universal quantifiers in introduction rules}
-\subsection{Continuing the `ground terms' example}
-
 
 Minor additions to the tutorial, unclear where
 ==============================================