equal
deleted
inserted
replaced
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 |