--- a/Nominal/Abs.thy	Sat Sep 04 14:26:09 2010 +0800
+++ b/Nominal/Abs.thy	Sun Sep 05 06:42:53 2010 +0800
@@ -6,6 +6,14 @@
         "Quotient_Product" 
 begin
 
+section {* Support w.r.t. relations *}
+
+definition 
+  "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
+
+
+section {* Abstractions *}
+
 fun
   alpha_set 
 where