equal
deleted
inserted
replaced
9 |
9 |
10 theory Map |
10 theory Map |
11 imports List |
11 imports List |
12 begin |
12 begin |
13 |
13 |
14 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
14 types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0) |
15 translations (type) "a ~=> b " <= (type) "a => b option" |
15 translations (type) "a ~=> b " <= (type) "a => b option" |
16 |
16 |
17 syntax (xsymbols) |
17 syntax (xsymbols) |
18 "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0) |
18 "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0) |
19 |
19 |