--- a/Nominal/Fv.thy	Thu Mar 18 14:29:42 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 14:48:27 2010 +0100
@@ -50,9 +50,9 @@
      with fv of the appropriate type
    - otherwise empty
 
-2) fv functions generated for all new datatypes:
+2) fv_ty functions generated for all types being defined:
 
-   An fv for a constructor is a union of values for the arguments.
+   fv_ty for a constructor is a union of values for the arguments.
 
    For an argument that is bound in a shallow binding we return empty.
 
@@ -92,6 +92,29 @@
    - for other arguments in the bn function we return: True
    - for other arguments not in the bn function we return: argl = argr
 
+2) alpha_ty relations are generated for all the types being defined:
+
+   !!! permutations !!!
+
+   An alpha_ty for a constructor is true if a conjunction of
+   propositions for each argument holds.
+
+   For an argument we allow bindings where only one of the following
+   holds:
+
+   - Argument is bound in some shallow bindings: We return true
+   - Argument is bound in some deep recursive bindings
+     !!! still to describe !!!
+   - Argument is bound in some deep non-recursive bindings.
+     We return: alpha_bn argl argr
+   - Argument has some shallow and/or non-recursive bindings.
+     !!! still to describe !!!
+   - Argument has some recursive bindings. The bindings were
+     already treated in 2nd case so we return: True
+   - Argument has no bindings and is not bound.
+     If it is recursive for type ty, we return: alpha_ty argl argr
+     Otherwise we return: argl = argr
+
 *)
 
 ML {*