src/HOL/Fun.thy
changeset 41229 d797baa3d57c
parent 40969 fb2d3ccda5a7
child 41505 6d19301074cf
     1.1 --- a/src/HOL/Fun.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -558,8 +558,8 @@
     1.4    fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
     1.5    "fun_upd f a b == % x. if x=a then b else f x"
     1.6  
     1.7 -nonterminals
     1.8 -  updbinds updbind
     1.9 +nonterminal updbinds and updbind
    1.10 +
    1.11  syntax
    1.12    "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
    1.13    ""         :: "updbind => updbinds"             ("_")