--- a/TODO	Sat Dec 17 16:58:11 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-Function definitions
-
-- nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?
-
-- nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]
-
-- equations that talk about True/False, for example
-    | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
-  do not work (since 'function' does not work)
-
-- equivariance for functions can be derived automatically (knowing termination and
-  equivariance of the graph).
-
-- for multiple simultanously defined functions, compatibility cases should fold the
-  definition and derive eqvt_at for the folded one
-
-- equivariance of the graph for multiple functions does not use equivariance
-  infrastructure
-
-Nominal_Datatype Parser should check that:
-
-- types of bindings match types of binding functions
-- fsets are not bound in lst bindings
-- bound arguments are not datatypes
-- binder is referred to by name and not by type
-
-Smaller things:
-
-- maybe <t1_t2>.perm_simps should be called permute_<type>.simps;
-  that would conform with the terminology in Nominal2
-
-- nominal_induct does not work without an induction rule
-
-- nominal_induct throws strange "THM" exceptions if not enough
-  variables are given
-
-- nominal_induct cannot avoid a term (for example function applied
-  to an argument).
-
-- .induct and .exhaust could be the default methods for induction/cases
-  on nominal datatypes
-
-Other:
-
-- nested recursion, like types "trm list" in a constructor
-
-- store information about defined nominal datatypes, so that
-  it can be used to define new types that depend on these
-