Quot/Nominal/Fv.thy
changeset 1206 9c968284553c
parent 1199 5770c73f2415
child 1207 fb33684e4ece
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 10:39:05 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 10:57:39 2010 +0100
@@ -90,6 +90,8 @@
 
 *}
 
+(* TODO: Notice datatypes without bindings and replace alpha with equality *)
+
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_fv_alpha full_tname bindsall lthy =