| changeset 252 | a4dc62a46ee4 |
| parent 251 | f04b33ce250f |
| child 253 | 132634d24019 |
| 251:f04b33ce250f | 252:a4dc62a46ee4 |
|---|---|
1 Rec = Fixedpt + |
|
2 consts |
|
3 fix :: "('a=>'a) => 'a" |
|
4 Dom :: "(('a=>'b) => ('a=>'b)) => 'a set" |
|
5 Domf :: "(('a=>'b) => ('a=>'b)) => 'a set => 'a set" |
|
6 rules |
|
7 Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}" |
|
8 Dom_def "Dom(F) == lfp(Domf(F))" |
|
9 end |