src/HOL/Library/Monad_Syntax.thy
changeset 81995 d67dadd69d07
parent 81989 96afb0707532
equal deleted inserted replaced
81994:5e50a2b52809 81995:d67dadd69d07
    68     \<rightleftharpoons> "_do_final (let p = t in s)"
    68     \<rightleftharpoons> "_do_final (let p = t in s)"
    69   "_do_block (_do_final e)" \<rightharpoonup> "e"
    69   "_do_block (_do_final e)" \<rightharpoonup> "e"
    70   "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
    70   "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
    71 
    71 
    72 adhoc_overloading
    72 adhoc_overloading
    73   bind Set.bind Predicate.bind Option.bind List.bind
    73   bind \<rightleftharpoons> Set.bind Predicate.bind Option.bind List.bind
    74 
    74 
    75 end
    75 end