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