--- a/Nominal-General/Nominal2_Base.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal-General/Nominal2_Base.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -848,6 +848,18 @@
   qed
 qed
 
+section {* Support w.r.t. relations *}
+
+text {* 
+  This definition is used for unquotient types, where
+  alpha-equivalence does not coincide with equality.
+*}
+
+definition 
+  "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
+
+
+
 section {* Finitely-supported types *}
 
 class fs = pt +