src/HOL/Library/State_Monad.thy
changeset 21835 84fd5de0691c
parent 21818 4d2ad5445c81
child 22377 61610b1beedf
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Dec 13 20:38:18 2006 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Dec 13 20:38:19 2006 +0100
     1.3 @@ -78,10 +78,6 @@
     1.4    run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
     1.5    "run f = f"
     1.6  
     1.7 -print_ast_translation {*[
     1.8 -  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
     1.9 -]*}
    1.10 -
    1.11  syntax (xsymbols)
    1.12    mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    1.13      (infixl "\<guillemotright>=" 60)
    1.14 @@ -91,6 +87,10 @@
    1.15  abbreviation (input)
    1.16    "return \<equiv> Pair"
    1.17  
    1.18 +print_ast_translation {*[
    1.19 +  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
    1.20 +]*}
    1.21 +
    1.22  text {*
    1.23    Given two transformations @{term f} and @{term g}, they
    1.24    may be directly composed using the @{term "op \<guillemotright>"} combinator,