--- a/TODO	Thu Mar 18 10:12:41 2010 +0100
+++ b/TODO	Thu Mar 18 10:15:57 2010 +0100
@@ -21,3 +21,10 @@
 
 - automate the proofs that are currently proved with sorry:
   alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
+
+- store information about defined nominal datatypes, so that
+  it can be used to define new types that depend on these
+
+- make 3 versions of Abs
+
+- make parser aware of recursive and of different versions of abs