src/HOL/Fun.thy
changeset 9340 9666f78ecfab
parent 9309 4078d5e8b293
child 9352 416b2ecd97a1
equal deleted inserted replaced
9339:0d8b0eb2932d 9340:9666f78ecfab
    26   "f(x:=y)"                     == "fun_upd f x y"
    26   "f(x:=y)"                     == "fun_upd f x y"
    27 
    27 
    28 defs
    28 defs
    29   fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    29   fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    30 
    30 
       
    31 (* Hint: to define the sum of two functions (or maps), use sum_case.
       
    32          A nice infix syntax could be defined (in Datatype.thy or below) by
       
    33 consts
       
    34   fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
       
    35 translations
       
    36  "fun_sum" == "sum_case"
       
    37 *)
    31   
    38   
    32 constdefs
    39 constdefs
    33   id ::  'a => 'a
    40   id ::  'a => 'a
    34     "id == %x. x"
    41     "id == %x. x"
    35 
    42