equal
deleted
inserted
replaced
35 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y" |
35 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y" |
36 |
36 |
37 dom_def "dom(m) == {a. m a ~= None}" |
37 dom_def "dom(m) == {a. m a ~= None}" |
38 ran_def "ran(m) == {b. ? a. m a = Some b}" |
38 ran_def "ran(m) == {b. ? a. m a = Some b}" |
39 |
39 |
40 primrec map_of list |
40 primrec |
41 "map_of [] = empty" |
41 "map_of [] = empty" |
42 "map_of (p#ps) = (map_of ps)[fst p |-> snd p]" |
42 "map_of (p#ps) = (map_of ps)[fst p |-> snd p]" |
43 |
43 |
44 end |
44 end |