--- a/src/HOL/Library/State_Monad.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/State_Monad.thy Fri Nov 17 02:20:03 2006 +0100
@@ -68,12 +68,16 @@
definition
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
- (infixl ">>=" 60)
+ (infixl ">>=" 60) where
"f >>= g = split g \<circ> f"
+
+definition
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
- (infixl ">>" 60)
+ (infixl ">>" 60) where
"f >> g = g \<circ> f"
- run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+
+definition
+ run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
"run f = f"
print_ast_translation {*[