# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268903757 -3600
# Node ID 8639077e0f43f2a4ad93833f2d1da6fcc261512b
# Parent  cc0dcf248da32e0b788d660cb42e90c8e6858333
Update TODO.

diff -r cc0dcf248da3 -r 8639077e0f43 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Thu Mar 18 10:12:41 2010 +0100
+++ b/Nominal/Perm.thy	Thu Mar 18 10:15:57 2010 +0100
@@ -96,7 +96,6 @@
     val perm_eqs = maps perm_eq descr;
     val lthy =
       Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-    (* TODO: Use the version of prmrec that gives the names explicitely. *)
     val ((perm_frees, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
diff -r cc0dcf248da3 -r 8639077e0f43 TODO
--- 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