equal
deleted
inserted
replaced
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "Quotient" |
4 "Quotient" |
5 "Quotient_List" |
5 "Quotient_List" |
6 "Quotient_Product" |
6 "Quotient_Product" |
7 begin |
7 begin |
|
8 |
|
9 section {* Support w.r.t. relations *} |
|
10 |
|
11 definition |
|
12 "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}" |
|
13 |
|
14 |
|
15 section {* Abstractions *} |
8 |
16 |
9 fun |
17 fun |
10 alpha_set |
18 alpha_set |
11 where |
19 where |
12 alpha_set[simp del]: |
20 alpha_set[simp del]: |