--- a/doc-src/TutorialI/todo.tobias Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Tue Mar 13 18:35:48 2001 +0100
@@ -61,14 +61,13 @@
differences between our HOL and the other one.
Syntax translations! Harpoons already used!
+say something about "abbreviations" when defs are introduced.
warning: simp of asms from l to r; may require reordering (rotate_tac)
Adjust FP textbook refs: new Bird, Hudak
Discrete math textbook: Rosen?
-say something about "abbreviations" when defs are introduced.
-
adjust type of ^ in tab:overloading
an example of induction: !y. A --> B --> C ??