src/HOLCF/Cont.thy
changeset 36452 d37c6eed8117
parent 35914 91a7311177c4
child 36658 e37b4338c71f
equal deleted inserted replaced
36451:ddc965e172c4 36452:d37c6eed8117
    12 text {*
    12 text {*
    13    Now we change the default class! Form now on all untyped type variables are
    13    Now we change the default class! Form now on all untyped type variables are
    14    of default class po
    14    of default class po
    15 *}
    15 *}
    16 
    16 
    17 defaultsort po
    17 default_sort po
    18 
    18 
    19 subsection {* Definitions *}
    19 subsection {* Definitions *}
    20 
    20 
    21 definition
    21 definition
    22   monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
    22   monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where