src/HOL/Library/State_Monad.thy
changeset 21404 eb85850d3eb7
parent 21283 b15355b9a59d
child 21418 4bc2882f80af
     1.1 --- a/src/HOL/Library/State_Monad.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -68,12 +68,16 @@
     1.4  
     1.5  definition
     1.6    mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
     1.7 -    (infixl ">>=" 60)
     1.8 +    (infixl ">>=" 60) where
     1.9    "f >>= g = split g \<circ> f"
    1.10 +
    1.11 +definition
    1.12    fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.13 -    (infixl ">>" 60)
    1.14 +    (infixl ">>" 60) where
    1.15    "f >> g = g \<circ> f"
    1.16 -  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.17 +
    1.18 +definition
    1.19 +  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.20    "run f = f"
    1.21  
    1.22  print_ast_translation {*[