# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269021373 -3600
# Node ID 73992021c8f08e90db178db2e5da2a99805eddf5
# Parent  572064152e8a49fb1dac554b3151bad3afc22aa8
Described automatically created funs.

diff -r 572064152e8a -r 73992021c8f0 TODO
--- 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;