--- a/Quot/Nominal/Fv.thy	Thu Feb 18 12:06:59 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Thu Feb 18 13:36:38 2010 +0100
@@ -28,6 +28,30 @@
 and a NONE binding has to be on an argument that is an atom
 or an atom set.
 
+How the procedure works:
+  For each of the defined datatypes,
+  For each of the constructors,
+  It creates a union of free variables for each argument.
+
+  For an argument the free variables are the variables minus
+  bound variables.
+
+  The variables are:
+    For an atom, a singleton set with the atom itself.
+    For an atom set, the atom set itself.
+    For a recursive argument, the appropriate fv function applied to it.
+    (* TODO: This one is not implemented *)
+    For other arguments it should be an appropriate fv function stored
+      in the database.
+  The bound variables are a union of results of all bindings that
+  involve the given argument. For a paricular binding the result is:
+    For a function applied to an argument this function with the argument.
+    For an atom, a singleton set with the atom itself.
+    For an atom set, the atom set itself.
+    For a recursive argument, the appropriate fv function applied to it.
+    (* TODO: This one is not implemented *)
+    For other arguments it should be an appropriate fv function stored
+      in the database.
 *)
 
 ML {*