lib/scripts/unsymbolize.pl

--- a/lib/scripts/unsymbolize.pl	Sun Dec 10 21:40:34 2000 +0100
+++ b/lib/scripts/unsymbolize.pl	Mon Dec 11 20:08:19 2000 +0100
@@ -32,6 +32,10 @@
     s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
     s/\\?\\<rightarrow>/->/g;
     s/\\?\\<epsilon> ?/SOME /g;
+    # outer syntax
+    s/\\?\\<rightleftharpoons>/==/g;
+    s/\\?\\<rightharpoonup>/=>/g;
+    s/\\?\\<leftharpoondown>/<=/g;
 
     $result = $_;