diff -r d1ff1ff5c5ad -r 140a1ed65665 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Jan 10 12:43:51 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Jan 10 12:53:50 2001 +0100
@@ -40,9 +40,6 @@
 explanation of term "contrapositive"/contraposition in Rules?
 Index the notion and maybe the rules contrapos_xy
 
-If Advanced and Types chapter ar swapped:
-Make forward ref from ... = True in Axioms to preprocessor section.
-
 get rid of use_thy in tutorial?
 
 Orderings on numbers (with hint that it is overloaded):
@@ -75,7 +72,7 @@
 Minor additions to the tutorial, unclear where
 ==============================================
 
-case_tac on bool?
+unfold?
 
 Tacticals: , ? +
 Note: + is used in typedef section!
@@ -83,10 +80,6 @@
 A list of further useful commands (rules? tricks?)
 prefer, defer, print_simpset (-> print_simps?)
 
-Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
-Where explained? Should go into a separate section as Inductive needs it as
-well.
-
 demonstrate x : set xs in Sets. Or Tricks chapter?
 
 Appendix with HOL and Isar keywords.