--- 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
==============================================