src/HOL/Fun.thy
changeset 35115 446c5063e4fd
parent 34209 c7f621786035
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Fun.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -387,18 +387,16 @@
     1.4    "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
     1.5    ""         :: "updbind => updbinds"             ("_")
     1.6    "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
     1.7 -  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000,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"
    1.12 -  "f(x:=y)"                     == "fun_upd f x y"
    1.13 +  "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
    1.14 +  "f(x:=y)" == "CONST fun_upd f x y"
    1.15  
    1.16  (* Hint: to define the sum of two functions (or maps), use sum_case.
    1.17           A nice infix syntax could be defined (in Datatype.thy or below) by
    1.18 -consts
    1.19 -  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    1.20 -translations
    1.21 - "fun_sum" == sum_case
    1.22 +notation
    1.23 +  sum_case  (infixr "'(+')"80)
    1.24  *)
    1.25  
    1.26  lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"