# HG changeset patch
# User wenzelm
# Date 1275294261 -7200
# Node ID 12d850a27eefc29626cdd3cd768d395e19c82392
# Parent  c4261f3bbdd7ec12a1178d07192ca2e313894beb
tuned abbrevs for long arrows, according to usual ASCII syntax;

diff -r c4261f3bbdd7 -r 12d850a27eef etc/symbols
--- a/etc/symbols	Mon May 31 09:47:41 2010 +0200
+++ b/etc/symbols	Mon May 31 10:24:21 2010 +0200
@@ -162,10 +162,10 @@
 \<Longleftarrow>        code: 0x0027f8  font: Isabelle 
 \<Rightarrow>           code: 0x0021d2  font: Isabelle  abbrev: =>
 \<Longrightarrow>       code: 0x0027f9  font: Isabelle  abbrev: ==>
-\<leftrightarrow>       code: 0x002194  font: Isabelle  abbrev: <->
-\<longleftrightarrow>   code: 0x0027f7  font: Isabelle  abbrev: <-->
-\<Leftrightarrow>       code: 0x0021d4  font: Isabelle  abbrev: <=>
-\<Longleftrightarrow>   code: 0x0027fa  font: Isabelle  abbrev: <==>
+\<leftrightarrow>       code: 0x002194  font: Isabelle
+\<longleftrightarrow>   code: 0x0027f7  font: Isabelle  abbrev: <->
+\<Leftrightarrow>       code: 0x0021d4  font: Isabelle
+\<Longleftrightarrow>   code: 0x0027fa  font: Isabelle  abbrev: <=>
 \<mapsto>               code: 0x0021a6  font: Isabelle  abbrev: |->
 \<longmapsto>           code: 0x0027fc  font: Isabelle  abbrev: |-->
 \<midarrow>             code: 0x002500  font: Isabelle