# HG changeset patch
# User nipkow
# Date 974895415 -3600
# Node ID ff24ac6678dd8bcb78ad9b8978c3f519f898d21b
# Parent  6306977d867bd22ac3a914902f1798d08d121a90
*** empty log message ***

diff -r 6306977d867b -r ff24ac6678dd doc-src/TutorialI/todo.tobias
--- 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!