# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1296794704 0
# Node ID dd5b60bccfd49166074c60c546a6dd121d5fe9ab
# Parent  8c1cda7ec284da4dc02ad55a3c58366ca2b362ce
updated TODO

diff -r 8c1cda7ec284 -r dd5b60bccfd4 TODO
--- a/TODO	Fri Feb 04 03:52:38 2011 +0000
+++ b/TODO	Fri Feb 04 04:45:04 2011 +0000
@@ -1,3 +1,7 @@
+Function definitions
+
+- export proofs bout alpha_bn
+
 
 Parser should check that:
 
@@ -16,12 +20,6 @@
 
 - nested recursion, like types "trm list" in a constructor
 
-- define permute_bn automatically and prove properties of it
-
-- prove renaming-of-binders lemmas
-
-- strong induction rules
-
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these