diff -r 7626cb4e1407 -r 875bf54b5d74 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Tue Oct 17 13:28:57 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Tue Oct 17 16:59:02 2000 +0200
@@ -50,9 +50,6 @@
 
 an example of induction: !y. A --> B --> C ??
 
-Advanced Ind expects rule_format incl (no_asm) (which it currently explains!
-Where explained?
-
 Appendix: Lexical: long ids.
 
 Warning: infixes automatically become reserved words!
@@ -83,7 +80,8 @@
 
 Mention that simp etc (big step tactics) insist on change?
 
-Explain what "by" and "." really do, and introduce "done".
+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
@@ -91,7 +89,11 @@
 An overview of the automatic methods: simp, auto, fast, blast, force,
 clarify, clarsimp (intro, elim?)
 
-explain rulify before induction section?
+Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
+Where explained?
+Inductive also needs rule_format!
+
+Where is "simplified" explained? Needed by Inductive/AB.thy
 
 demonstrate x : set xs in Sets. Or Tricks chapter?