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