Described automatically created funs.
--- a/TODO Fri Mar 19 18:43:29 2010 +0100
+++ b/TODO Fri Mar 19 18:56:13 2010 +0100
@@ -1,3 +1,15 @@
+Automatically created functions:
+
+ ty1_tyn.bn[simp] lifted equations for bn funs
+ ty1_tyn.fv[simp] lifted equations for fv funs
+ ty1_tyn.perm[simp] lifted permutation equations
+ ty1_tyn.distinct[simp] lifted distincts
+ ty1_tyn.eq_iff
+ ty1_tyn.induct
+ ty1_tyn.inducts
+ instance ty1 and tyn :: fs
+ ty1_tyn.supp for too many bindings empty
+
Smaller things:
- maybe <type>_perm whould be called permute_<type>.simps;