--- a/doc-src/TutorialI/todo.tobias Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Fri Jan 26 15:50:28 2001 +0100
@@ -35,15 +35,12 @@
Minor fixes in the tutorial
===========================
-adjust type of ^ in tab:overloading
-
-explanation of term "contrapositive"/contraposition in Rules?
-Index the notion and maybe the rules contrapos_xy
+Adjust FP textbook refs: new Bird, Hudak
+Discrete math textbook: Rosen?
-get rid of use_thy in tutorial?
+say something about "abbreviations" when defs are introduced.
-Orderings on numbers (with hint that it is overloaded):
-bounded quantifers ALL x<y, <=.
+adjust type of ^ in tab:overloading
an example of induction: !y. A --> B --> C ??
@@ -74,16 +71,6 @@
unfold?
-Tacticals: , ? +
-Note: + is used in typedef section!
-
-A list of further useful commands (rules? tricks?)
-prefer, defer, print_simpset (-> print_simps?)
-
-demonstrate x : set xs in Sets. Or Tricks chapter?
-
-Appendix with HOL and Isar keywords.
-
Possible exercises
==================