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