tuned abbrevs for long arrows, according to usual ASCII syntax;
authorwenzelm
Mon May 31 10:24:21 2010 +0200 (2010-05-31)
changeset 3720412d850a27eef
parent 37203 c4261f3bbdd7
child 37205 1509e49c8d33
tuned abbrevs for long arrows, according to usual ASCII syntax;
etc/symbols
     1.1 --- a/etc/symbols	Mon May 31 09:47:41 2010 +0200
     1.2 +++ b/etc/symbols	Mon May 31 10:24:21 2010 +0200
     1.3 @@ -162,10 +162,10 @@
     1.4  \<Longleftarrow>        code: 0x0027f8  font: Isabelle 
     1.5  \<Rightarrow>           code: 0x0021d2  font: Isabelle  abbrev: =>
     1.6  \<Longrightarrow>       code: 0x0027f9  font: Isabelle  abbrev: ==>
     1.7 -\<leftrightarrow>       code: 0x002194  font: Isabelle  abbrev: <->
     1.8 -\<longleftrightarrow>   code: 0x0027f7  font: Isabelle  abbrev: <-->
     1.9 -\<Leftrightarrow>       code: 0x0021d4  font: Isabelle  abbrev: <=>
    1.10 -\<Longleftrightarrow>   code: 0x0027fa  font: Isabelle  abbrev: <==>
    1.11 +\<leftrightarrow>       code: 0x002194  font: Isabelle
    1.12 +\<longleftrightarrow>   code: 0x0027f7  font: Isabelle  abbrev: <->
    1.13 +\<Leftrightarrow>       code: 0x0021d4  font: Isabelle
    1.14 +\<Longleftrightarrow>   code: 0x0027fa  font: Isabelle  abbrev: <=>
    1.15  \<mapsto>               code: 0x0021a6  font: Isabelle  abbrev: |->
    1.16  \<longmapsto>           code: 0x0027fc  font: Isabelle  abbrev: |-->
    1.17  \<midarrow>             code: 0x002500  font: Isabelle