# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271002005 -7200
# Node ID 9a32e02cc95b9f41830a28c0d530b119e8d32705
# Parent  6d2a39db3862e1b45e94293978f46ec490c59d24
added small ittems about equivaraince of alpha_gens and name of lam.perm

diff -r 6d2a39db3862 -r 9a32e02cc95b TODO
--- 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