src/HOL/Library/State_Monad.thy
changeset 41229 d797baa3d57c
parent 40361 c409827db57d
child 54703 499f92dc6e45
     1.1 --- a/src/HOL/Library/State_Monad.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -114,8 +114,7 @@
     1.4  
     1.5  subsection {* Do-syntax *}
     1.6  
     1.7 -nonterminals
     1.8 -  sdo_binds sdo_bind
     1.9 +nonterminal sdo_binds and sdo_bind
    1.10  
    1.11  syntax
    1.12    "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)