diff -r cda25f9aa678 -r a3711f07449b Nominal/Abs.thy --- 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. \(R ((a \ b) \ x) x)}}" + + +section {* Abstractions *} + fun alpha_set where