harpoons;
authorwenzelm
Mon, 11 Dec 2000 20:08:19 +0100
changeset 10639f902346264e9
parent 10638 17063aee1d86
child 10640 562e20e543b1
harpoons;
doc-src/IsarRef/isar-ref.tex
lib/scripts/unsymbolize.pl
     1.1 --- a/doc-src/IsarRef/isar-ref.tex	Sun Dec 10 21:40:34 2000 +0100
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Mon Dec 11 20:08:19 2000 +0100
     1.3 @@ -14,6 +14,9 @@
     1.4  \newcommand{\isamath}[1]{\emph{$#1$}}
     1.5  \newcommand{\isasymColon}{\isamath{\mathrel{::}}}
     1.6  \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
     1.7 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
     1.8 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
     1.9 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
    1.10  
    1.11  \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
    1.12  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
     2.1 --- a/lib/scripts/unsymbolize.pl	Sun Dec 10 21:40:34 2000 +0100
     2.2 +++ b/lib/scripts/unsymbolize.pl	Mon Dec 11 20:08:19 2000 +0100
     2.3 @@ -32,6 +32,10 @@
     2.4      s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
     2.5      s/\\?\\<rightarrow>/->/g;
     2.6      s/\\?\\<epsilon> ?/SOME /g;
     2.7 +    # outer syntax
     2.8 +    s/\\?\\<rightleftharpoons>/==/g;
     2.9 +    s/\\?\\<rightharpoonup>/=>/g;
    2.10 +    s/\\?\\<leftharpoondown>/<=/g;
    2.11  
    2.12      $result = $_;
    2.13