# HG changeset patch
# User wenzelm
# Date 1377858796 -7200
# Node ID 53c314f1e8bfa5aa51e2ae4728b3a4451ae63695
# Parent  17b887110cc14b870e56c4e1f17e2a787657a377
fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;

diff -r 17b887110cc1 -r 53c314f1e8bf etc/symbols
--- a/etc/symbols	Fri Aug 30 12:24:15 2013 +0200
+++ b/etc/symbols	Fri Aug 30 12:33:16 2013 +0200
@@ -161,11 +161,11 @@
 \<Leftarrow>            code: 0x0021d0  group: arrow
 \<Longleftarrow>        code: 0x0027f8  group: arrow
 \<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: =>
-\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>
+\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>  abbrev: ≡>
 \<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <->
 \<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->  abbrev: <-->
-\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <=>
-\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <=>  abbrev: <==>
+\<Leftrightarrow>       code: 0x0021d4  group: arrow
+\<Longleftrightarrow>   code: 0x0027fa  group: arrow
 \<mapsto>               code: 0x0021a6  group: arrow  abbrev: |->
 \<longmapsto>           code: 0x0027fc  group: arrow  abbrev: |-->
 \<midarrow>             code: 0x002500  group: arrow