| 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 |
"===>" = "===>" |