diff -r 0b40c19f09f3 -r 06f390008ceb doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Dec 14 19:38:37 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias	Fri Dec 15 12:32:35 2000 +0100
@@ -78,11 +78,6 @@
 Tacticals: , ? +
 Note: + is used in typedef section!
 
-Mention that simp etc (big step tactics) insist on change?
-
-Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
-does more.)
-
 A list of further useful commands (rules? tricks?)
 prefer, defer, print_simpset (-> print_simps?)
 
@@ -90,11 +85,9 @@
 Where explained? Should go into a separate section as Inductive needs it as
 well.
 
-Where is "simplified" explained? Needed by Inductive/AB.thy
-
 demonstrate x : set xs in Sets. Or Tricks chapter?
 
-Appendix with HOL keywords. Say something about other keywords.
+Appendix with HOL and Isar keywords.
 
 
 Possible exercises