equal
deleted
inserted
replaced
17 dom :: "('a ~=> 'b) => 'a set" |
17 dom :: "('a ~=> 'b) => 'a set" |
18 ran :: "('a ~=> 'b) => 'b set" |
18 ran :: "('a ~=> 'b) => 'b set" |
19 map_of :: "('a * 'b)list => 'a ~=> 'b" |
19 map_of :: "('a * 'b)list => 'a ~=> 'b" |
20 map_upds:: "('a ~=> 'b) => 'a list => 'b list => |
20 map_upds:: "('a ~=> 'b) => 'a list => 'b list => |
21 ('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900) |
21 ('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900) |
22 |
|
23 |
|
24 syntax |
22 syntax |
25 map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)" |
23 map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)" |
26 ("_/'(_/|->_')" [900,0,0]900) |
24 ("_/'(_/|->_')" [900,0,0]900) |
27 |
25 |
28 syntax (symbols) |
26 syntax (symbols) |