Described automatically created funs.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 19 Mar 2010 18:56:13 +0100
changeset 1555 73992021c8f0
parent 1554 572064152e8a
child 1556 a7072d498723
Described automatically created funs.
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;