1 (* additional abbreviations for syntactic completion *)
2
3 (*prevent replacement of very long arrows*)
4 "--->" = "--->"
5 "===>" = "===>"