# HG changeset patch
# User wenzelm
# Date 976561699 -3600
# Node ID f902346264e90122c6100e09f7b7c5dfb952408c
# Parent  17063aee1d8627cd447c0da749ddec71b275fda2
harpoons;

diff -r 17063aee1d86 -r f902346264e9 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Sun Dec 10 21:40:34 2000 +0100
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Dec 11 20:08:19 2000 +0100
@@ -14,6 +14,9 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isasymColon}{\isamath{\mathrel{::}}}
 \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
 
 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
diff -r 17063aee1d86 -r f902346264e9 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 = $_;