equal
deleted
inserted
replaced
1 (* Author: Andreas Lochbihler, KIT *) |
1 (* Author: Andreas Lochbihler, KIT *) |
2 |
2 |
3 header {* Pretty syntax for almost everywhere constant functions *} |
3 header {* Pretty syntax for almost everywhere constant functions *} |
4 |
4 |
5 theory FinFun_Syntax imports FinFun begin |
5 theory FinFun_Syntax |
|
6 imports FinFun |
|
7 begin |
6 |
8 |
7 type_notation |
9 type_notation |
8 finfun ("(_ =>f /_)" [22, 21] 21) |
10 finfun ("(_ =>f /_)" [22, 21] 21) |
9 |
11 |
10 type_notation (xsymbols) |
12 type_notation (xsymbols) |