src/HOL/HOL.thy
changeset 36452 d37c6eed8117
parent 36365 18bf20d0c2df
child 36532 fdfc37254090
equal deleted inserted replaced
36451:ddc965e172c4 36452:d37c6eed8117
    38 subsection {* Primitive logic *}
    38 subsection {* Primitive logic *}
    39 
    39 
    40 subsubsection {* Core syntax *}
    40 subsubsection {* Core syntax *}
    41 
    41 
    42 classes type
    42 classes type
    43 defaultsort type
    43 default_sort type
    44 setup {* Object_Logic.add_base_sort @{sort type} *}
    44 setup {* Object_Logic.add_base_sort @{sort type} *}
    45 
    45 
    46 arities
    46 arities
    47   "fun" :: (type, type) type
    47   "fun" :: (type, type) type
    48   itself :: (type) type
    48   itself :: (type) type