src/HOL/Set.thy
changeset 3370 5c5fdce3a4e4
parent 3222 726a9b069947
child 3820 46b255e140dc
equal deleted inserted replaced
3369:51ed014406fa 3370:5c5fdce3a4e4
    14 
    14 
    15 arities
    15 arities
    16   set :: (term) term
    16   set :: (term) term
    17 
    17 
    18 instance
    18 instance
    19   set :: (term) {ord, minus}
    19   set :: (term) {ord, minus, power}
    20 
    20 
    21 consts
    21 consts
    22   "{}"          :: 'a set                           ("{}")
    22   "{}"          :: 'a set                           ("{}")
    23   insert        :: ['a, 'a set] => 'a set
    23   insert        :: ['a, 'a set] => 'a set
    24   Collect       :: ('a => bool) => 'a set               (*comprehension*)
    24   Collect       :: ('a => bool) => 'a set               (*comprehension*)