--- a/doc-src/TutorialI/todo.tobias Tue Nov 21 19:04:59 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias Wed Nov 22 13:16:55 2000 +0100
@@ -47,8 +47,14 @@
Explain typographic conventions?
+Orderings on numbers (with hint that it is overloaded):
+>, >=, and bounded quantifers ALL x<y, <=, todo: x>y, x>=y.
+
an example of induction: !y. A --> B --> C ??
+Explain type_definition and mention pre-proved thms in subset.thy?
+-> Types/typedef
+
Appendix: Lexical: long ids.
Warning: infixes automatically become reserved words!