--- a/Nominal/Fv.thy	Thu Mar 18 14:05:49 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 14:29:42 2010 +0100
@@ -78,6 +78,20 @@
 
 (*
 An overview of the generation of alpha-equivalence:
+
+1) alpha_bn relations are generated for binding functions.
+
+   An alpha_bn for a constructor is true if a conjunction of
+   propositions for each argument holds.
+
+   For an argument a proposition is build as follows from
+   th:
+
+   - for a recursive argument in the bn function, we return: alpha_bn argl argr
+   - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr
+   - for other arguments in the bn function we return: True
+   - for other arguments not in the bn function we return: argl = argr
+
 *)
 
 ML {*