author | wenzelm |
Tue, 29 Dec 2015 22:41:22 +0100 | |
changeset 61968 | e13e70f32407 |
parent 61963 | 2548e7cc86fb |
child 61970 | 6226261144d7 |
permissions | -rw-r--r-- |
61961 | 1 |
(* additional abbreviations for syntactic completion *) |
2 |
||
3 |
(*prevent replacement of very long arrows*) |
|
61968
e13e70f32407
avoid immediate completion as ASCII versions that are still used;
wenzelm
parents:
61963
diff
changeset
|
4 |
"--->" = "--->" |
e13e70f32407
avoid immediate completion as ASCII versions that are still used;
wenzelm
parents:
61963
diff
changeset
|
5 |
"---->" = "---->" |
61963 | 6 |
"----->" = "----->" |
61961 | 7 |
"===>" = "===>" |