# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1296859140 -32400
# Node ID af5bbc257f7f36b381c2666dc0d9e45f7b82c4f9
# Parent  3dd6d524dfddc3b9c5a789df76af9676be9c107c# Parent  dd5b60bccfd49166074c60c546a6dd121d5fe9ab
merge

diff -r 3dd6d524dfdd -r af5bbc257f7f TODO
--- a/TODO	Sat Feb 05 07:38:22 2011 +0900
+++ b/TODO	Sat Feb 05 07:39:00 2011 +0900
@@ -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