etc/symbols
changeset 61964 37a0cbee00c2
parent 61963 2548e7cc86fb
child 61972 a70b89a3e02e
     1.1 --- a/etc/symbols	Tue Dec 29 20:58:18 2015 +0100
     1.2 +++ b/etc/symbols	Tue Dec 29 21:51:58 2015 +0100
     1.3 @@ -164,8 +164,10 @@
     1.4  \<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: ---->
     1.5  \<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
     1.6  \<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
     1.7 +\<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.
     1.8  \<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>
     1.9  \<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: .>  abbrev: ==>
    1.10 +\<Rrightarrow>          code: 0x0021db  group: arrow  abbrev: .>
    1.11  \<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <>  abbrev: <->
    1.12  \<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <>  abbrev: <->  abbrev: <-->
    1.13  \<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <>