--- a/TODO	Sun Apr 11 10:36:09 2010 +0200
+++ b/TODO	Sun Apr 11 18:06:45 2010 +0200
@@ -12,12 +12,18 @@
 
 Smaller things:
 
+- lam.perm should be called permute_lam.simps (that is 
+  the convention from Nominal2)
+
 - maybe <type>_perm whould be called permute_<type>.simps;
   that would conform with the terminology in Nominal2
 
 - we also need to lift the size function for nominal
   datatypes
 
+- Abs.thy contains lemmas for equivariance of the alphas;
+  they are not yet used anywhere
+
 Bigger things:
 
 - the alpha equivalence for