etc/symbols
changeset 53321 53c314f1e8bf
parent 53320 17b887110cc1
child 53323 5fa77d6ad63d
     1.1 --- a/etc/symbols	Fri Aug 30 12:24:15 2013 +0200
     1.2 +++ b/etc/symbols	Fri Aug 30 12:33:16 2013 +0200
     1.3 @@ -161,11 +161,11 @@
     1.4  \<Leftarrow>            code: 0x0021d0  group: arrow
     1.5  \<Longleftarrow>        code: 0x0027f8  group: arrow
     1.6  \<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: =>
     1.7 -\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>
     1.8 +\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>  abbrev: ≡>
     1.9  \<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <->
    1.10  \<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->  abbrev: <-->
    1.11 -\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <=>
    1.12 -\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <=>  abbrev: <==>
    1.13 +\<Leftrightarrow>       code: 0x0021d4  group: arrow
    1.14 +\<Longleftrightarrow>   code: 0x0027fa  group: arrow
    1.15  \<mapsto>               code: 0x0021a6  group: arrow  abbrev: |->
    1.16  \<longmapsto>           code: 0x0027fc  group: arrow  abbrev: |-->
    1.17  \<midarrow>             code: 0x002500  group: arrow