equal
deleted
inserted
replaced
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 type_notation (xsymbols) |
18 "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0) |
18 "~=>" (infixr "\<rightharpoonup>" 0) |
19 |
19 |
20 abbreviation |
20 abbreviation |
21 empty :: "'a ~=> 'b" where |
21 empty :: "'a ~=> 'b" where |
22 "empty == %x. None" |
22 "empty == %x. None" |
23 |
23 |