--- a/doc-src/TutorialI/todo.tobias Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias Sun Nov 26 10:48:38 2000 +0100
@@ -1,7 +1,6 @@
Implementation
==============
-Hide global names like Node.
Why is comp needed in addition to op O?
Explain in syntax section!
@@ -31,7 +30,9 @@
Induction rules for int: int_le/ge_induct?
Needed for ifak example. But is that example worth it?
-defs with = and pattern matching
+proper mutual simplification
+
+defs with = and pattern matching??
Minor fixes in the tutorial
@@ -48,7 +49,7 @@
Explain typographic conventions?
Orderings on numbers (with hint that it is overloaded):
->, >=, and bounded quantifers ALL x<y, <=, todo: x>y, x>=y.
+bounded quantifers ALL x<y, <=.
an example of induction: !y. A --> B --> C ??
@@ -71,6 +72,10 @@
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
==============================================