diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Wed Oct 11 09:09:06 2000 +0200
@@ -27,15 +27,16 @@
 
 defs with = and pattern matching
 
-Why can't I declare trev at the end of Recdef/Nested0 and define it in
-Recdef/Nested1??
-
 use arith_tac in recdef to solve termination conditions?
 -> new example in Recdef/termination
 
 a tactic for replacing a specific occurrence:
 apply(substitute [2] thm)
 
+it would be nice if @term could deal with ?-vars.
+then a number of (unchecked!) @texts could be converted to @terms.
+
+
 Minor fixes in the tutorial
 ===========================
 
@@ -45,8 +46,6 @@
 
 Explain typographic conventions?
 
-how the simplifier works
-
 an example of induction: !y. A --> B --> C ??
 
 Advanced Ind expects rulify, mp and spec. How much really?
@@ -80,15 +79,18 @@
 literature. In Recdef/termination.thy, at the end.
 %FIXME, with one exception: nested recursion.
 
-Sets: rels and ^*
+Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
+
+Prove EU exercise in CTL.
 
 
 Minor additions to the tutorial, unclear where
 ==============================================
 
-insert: lcp?
+Tacticals: , ? +
 
-Tacticals: , ? +
+"typedecl" is used in CTL/Base, but where is it introduced?
+In More Types chapter? Rephrase the CTL bit accordingly.
 
 print_simpset (-> print_simps?)
 (Another subsection Useful theorems, methods, and commands?)
@@ -107,7 +109,6 @@
 
 demonstrate x : set xs in Sets. Or Tricks chapter?
 
-Table with symbols \<forall> etc. Apendix?
 Appendix with HOL keywords. Say something about other keywords.
 
 
@@ -123,8 +124,6 @@
 Nested inductive datatypes: another example/exercise:
  size(t) <= size(subst s t)?
 
-Add Until to CTL.
-
 insertion sort: primrec, later recdef
 
 OTree: