| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15251 | bb6f072c8d10 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 header {* Maps *} |
9 header {* Maps *} |
10 |
10 |
11 theory Map |
11 theory Map |
12 import List |
12 imports List |
13 begin |
13 begin |
14 |
14 |
15 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
15 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
16 translations (type) "a ~=> b " <= (type) "a => b option" |
16 translations (type) "a ~=> b " <= (type) "a => b option" |
17 |
17 |