changeset 27220 | 31adee1f467a |
parent 14981 | e73f8140af78 |
child 29145 | b1c6f4563df7 |
--- a/lib/scripts/unsymbolize.pl Sat Jun 14 23:20:12 2008 +0200 +++ b/lib/scripts/unsymbolize.pl Sat Jun 14 23:33:43 2008 +0200 @@ -32,7 +32,9 @@ s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g; s/\\?\\<rightarrow>/->/g; s/\\?\\<not>/~/g; - s/\\?\\<epsilon> ?/SOME /g; + s/\\?\\<notin>/~:/g; + s/\\?\\<noteq>/~=/g; + s/\\?\\<some> ?/SOME /g; # outer syntax s/\\?\\<rightleftharpoons>/==/g; s/\\?\\<rightharpoonup>/=>/g;