changeset 39128 | 93a7365fb4ee |
parent 38499 | 8f0cd11238a7 |
child 41526 | 54b4686704af |
39127:e7ecbe86d22e | 39128:93a7365fb4ee |
---|---|
1 header {* Extending FOL by a modified version of HOL set theory *} |
1 header {* Extending FOL by a modified version of HOL set theory *} |
2 |
2 |
3 theory Set |
3 theory Set |
4 imports FOL |
4 imports FOL |
5 begin |
5 begin |
6 |
|
7 declare [[eta_contract]] |
|
6 |
8 |
7 typedecl 'a set |
9 typedecl 'a set |
8 arities set :: ("term") "term" |
10 arities set :: ("term") "term" |
9 |
11 |
10 consts |
12 consts |