--- 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.