src/HOL/Library/Monad_Syntax.thy
changeset 41229 d797baa3d57c
parent 39151 fd179beb8cb3
child 45145 d5086da3c32d
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -37,8 +37,7 @@
     1.4  notation (latex output)
     1.5    bind_do (infixr "\<bind>" 54)
     1.6  
     1.7 -nonterminals
     1.8 -  do_binds do_bind
     1.9 +nonterminal do_binds and do_bind
    1.10  
    1.11  syntax
    1.12    "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)