src/HOL/Library/State_Monad.thy
changeset 22492 43545e640877
parent 22377 61610b1beedf
child 22664 e965391e2864
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Mar 21 13:58:36 2007 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Mar 21 16:06:15 2007 +0100
     1.3 @@ -257,12 +257,12 @@
     1.4  fun
     1.5    list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
     1.6    "list f [] = id"
     1.7 -  "list f (x#xs) = (do f x; list f xs done)"
     1.8 +| "list f (x#xs) = (do f x; list f xs done)"
     1.9  lemmas [code] = list.simps
    1.10  
    1.11  fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
    1.12    "list_yield f [] = return []"
    1.13 -  "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    1.14 +| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    1.15  lemmas [code] = list_yield.simps
    1.16    
    1.17  text {* combinator properties *}