uniform abbrevs for left/right arrows;
authorwenzelm
Sat Aug 31 13:20:18 2013 +0200 (2013-08-31)
changeset 533458c333d659e8f
parent 53344 9a5eaa6b0154
child 53346 26c795734b3c
uniform abbrevs for left/right arrows;
etc/symbols
     1.1 --- a/etc/symbols	Sat Aug 31 13:05:04 2013 +0200
     1.2 +++ b/etc/symbols	Sat Aug 31 13:20:18 2013 +0200
     1.3 @@ -154,30 +154,30 @@
     1.4  \<rat>                  code: 0x00211a  group: letter
     1.5  \<real>                 code: 0x00211d  group: letter
     1.6  \<int>                  code: 0x002124  group: letter
     1.7 -\<leftarrow>            code: 0x002190  group: arrow
     1.8 -\<longleftarrow>        code: 0x0027f5  group: arrow
     1.9 -\<rightarrow>           code: 0x002192  group: arrow  abbrev: ->
    1.10 -\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: -->
    1.11 -\<Leftarrow>            code: 0x0021d0  group: arrow
    1.12 -\<Longleftarrow>        code: 0x0027f8  group: arrow
    1.13 -\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: =>
    1.14 -\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>
    1.15 -\<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <->
    1.16 -\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->  abbrev: <-->
    1.17 -\<Leftrightarrow>       code: 0x0021d4  group: arrow
    1.18 -\<Longleftrightarrow>   code: 0x0027fa  group: arrow
    1.19 -\<mapsto>               code: 0x0021a6  group: arrow  abbrev: |->
    1.20 -\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: |-->
    1.21 -\<midarrow>             code: 0x002500  group: arrow
    1.22 -\<Midarrow>             code: 0x002550  group: arrow
    1.23 -\<hookleftarrow>        code: 0x0021a9  group: arrow
    1.24 -\<hookrightarrow>       code: 0x0021aa  group: arrow
    1.25 -\<leftharpoondown>      code: 0x0021bd  group: arrow
    1.26 -\<rightharpoondown>     code: 0x0021c1  group: arrow
    1.27 -\<leftharpoonup>        code: 0x0021bc  group: arrow
    1.28 -\<rightharpoonup>       code: 0x0021c0  group: arrow
    1.29 -\<rightleftharpoons>    code: 0x0021cc  group: arrow  abbrev: ==
    1.30 -\<leadsto>              code: 0x00219d  group: arrow  abbrev: ~>
    1.31 +\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
    1.32 +\<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
    1.33 +\<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
    1.34 +\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
    1.35 +\<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
    1.36 +\<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
    1.37 +\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>
    1.38 +\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: .>  abbrev: ==>
    1.39 +\<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <>  abbrev: <->
    1.40 +\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <>  abbrev: <->  abbrev: <-->
    1.41 +\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <>
    1.42 +\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <>
    1.43 +\<mapsto>               code: 0x0021a6  group: arrow  abbrev: .>  abbrev: |->
    1.44 +\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: .>  abbrev: |-->
    1.45 +\<midarrow>             code: 0x002500  group: arrow  abbrev: <>
    1.46 +\<Midarrow>             code: 0x002550  group: arrow  abbrev: <>
    1.47 +\<hookleftarrow>        code: 0x0021a9  group: arrow  abbrev: <.
    1.48 +\<hookrightarrow>       code: 0x0021aa  group: arrow  abbrev: .>
    1.49 +\<leftharpoondown>      code: 0x0021bd  group: arrow  abbrev: <.
    1.50 +\<rightharpoondown>     code: 0x0021c1  group: arrow  abbrev: .>
    1.51 +\<leftharpoonup>        code: 0x0021bc  group: arrow  abbrev: <.
    1.52 +\<rightharpoonup>       code: 0x0021c0  group: arrow  abbrev: .>
    1.53 +\<rightleftharpoons>    code: 0x0021cc  group: arrow  abbrev: <> abbrev: ==
    1.54 +\<leadsto>              code: 0x00219d  group: arrow  abbrev: .> abbrev: ~>
    1.55  \<downharpoonleft>      code: 0x0021c3  group: arrow
    1.56  \<downharpoonright>     code: 0x0021c2  group: arrow
    1.57  \<upharpoonleft>        code: 0x0021bf  group: arrow