src/HOL/Library/State_Monad.thy
changeset 21601 6588b947d631
parent 21418 4bc2882f80af
child 21818 4d2ad5445c81
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Nov 29 23:33:09 2006 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Nov 30 14:17:22 2006 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4  subsection {* Combinators *}
     1.5  
     1.6  definition
     1.7 -  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c"
     1.8 +  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
     1.9    "lift f x = return (f x)"
    1.10  
    1.11  fun