src/HOL/Fun.thy
changeset 8258 666d3a4f3b9d
parent 7374 dec7b838f5cb
child 8924 c434283b4cfa
     1.1 --- a/src/HOL/Fun.thy	Fri Feb 18 18:29:28 2000 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Feb 18 20:24:16 2000 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
     1.5    ""               :: updbind => updbinds             ("_")
     1.6    "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
     1.7 -  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
     1.8 +  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
     1.9  
    1.10  translations
    1.11    "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"