src/HOL/Library/Monad_Syntax.thy
changeset 60500 903bb1495239
parent 59359 07b9893cd8a7
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,17 +2,17 @@
     1.4     Author: Christian Sternagel, University of Innsbruck
     1.5  *)
     1.6  
     1.7 -section {* Monad notation for arbitrary types *}
     1.8 +section \<open>Monad notation for arbitrary types\<close>
     1.9  
    1.10  theory Monad_Syntax
    1.11  imports Main "~~/src/Tools/Adhoc_Overloading"
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    We provide a convenient do-notation for monadic expressions
    1.17    well-known from Haskell.  @{const Let} is printed
    1.18    specially in do-expressions.
    1.19 -*}
    1.20 +\<close>
    1.21  
    1.22  consts
    1.23    bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)