src/HOL/Library/Monad_Syntax.thy
changeset 46143 c932c80d3eae
parent 45990 b7b905b23b2a
child 52622 e0ff1625e96d
equal deleted inserted replaced
46142:94479a979129 46143:c932c80d3eae
    72 setup {*
    72 setup {*
    73   Adhoc_Overloading.add_overloaded @{const_name bind}
    73   Adhoc_Overloading.add_overloaded @{const_name bind}
    74   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
    74   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
    75   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
    75   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
    76   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
    76   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
    77   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
    77   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
    78 *}
    78 *}
    79 
    79 
    80 end
    80 end