lib/scripts/unsymbolize.pl
changeset 27220 31adee1f467a
parent 14981 e73f8140af78
child 29145 b1c6f4563df7
equal deleted inserted replaced
27219:a248dba028ff 27220:31adee1f467a
    30     s/\\?\\<longleftrightarrow>/<->/g;
    30     s/\\?\\<longleftrightarrow>/<->/g;
    31     s/\\?\\<longrightarrow>/-->/g;
    31     s/\\?\\<longrightarrow>/-->/g;
    32     s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    32     s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    33     s/\\?\\<rightarrow>/->/g;
    33     s/\\?\\<rightarrow>/->/g;
    34     s/\\?\\<not>/~/g;
    34     s/\\?\\<not>/~/g;
    35     s/\\?\\<epsilon> ?/SOME /g;
    35     s/\\?\\<notin>/~:/g;
       
    36     s/\\?\\<noteq>/~=/g;
       
    37     s/\\?\\<some> ?/SOME /g;
    36     # outer syntax
    38     # outer syntax
    37     s/\\?\\<rightleftharpoons>/==/g;
    39     s/\\?\\<rightleftharpoons>/==/g;
    38     s/\\?\\<rightharpoonup>/=>/g;
    40     s/\\?\\<rightharpoonup>/=>/g;
    39     s/\\?\\<leftharpoondown>/<=/g;
    41     s/\\?\\<leftharpoondown>/<=/g;
    40 
    42