diff -r 6e37bfb62474 -r 486d4647bb37 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -33,6 +33,11 @@
   val mk_supp_ty: typ -> term -> term
   val mk_supp: term -> term
 
+  val supp_rel_ty: typ -> typ
+  val supp_rel_const: typ -> term
+  val mk_supp_rel_ty: typ -> term -> term -> term
+  val mk_supp_rel: term -> term -> term		       
+
   val supports_const: typ -> term
   val mk_supports_ty: typ -> term -> term -> term
   val mk_supports: term -> term -> term
@@ -124,8 +129,13 @@
 
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
-fun mk_supp_ty ty t = supp_const ty $ t;
-fun mk_supp t = mk_supp_ty (fastype_of t) t;
+fun mk_supp_ty ty t = supp_const ty $ t
+fun mk_supp t = mk_supp_ty (fastype_of t) t
+
+fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"};
+fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty)
+fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t
+fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t
 
 fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool});
 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;