equal
deleted
inserted
replaced
6 The datatype of `maps' (written ~=>); strongly resembles maps in VDM. |
6 The datatype of `maps' (written ~=>); strongly resembles maps in VDM. |
7 *) |
7 *) |
8 |
8 |
9 header {* Maps *} |
9 header {* Maps *} |
10 |
10 |
11 theory Map = List: |
11 theory Map |
|
12 import List |
|
13 begin |
12 |
14 |
13 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
15 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
14 translations (type) "a ~=> b " <= (type) "a => b option" |
16 translations (type) "a ~=> b " <= (type) "a => b option" |
15 |
17 |
16 consts |
18 consts |