src/CCL/Set.thy
changeset 39128 93a7365fb4ee
parent 38499 8f0cd11238a7
child 41526 54b4686704af
equal deleted inserted replaced
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