| changeset 2475 | 486d4647bb37 |
| parent 2473 | a3711f07449b |
| child 2479 | a9b6a00b1ba0 |
| 2474:6e37bfb62474 | 2475:486d4647bb37 |
|---|---|
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 |
8 |
14 |
9 |
15 section {* Abstractions *} |
10 section {* Abstractions *} |
16 |
11 |
17 fun |
12 fun |