# HG changeset patch
# User wenzelm
# Date 979154471 -3600
# Node ID 857688d775b044f568019db108cffc2ab4e3af8a
# Parent  f2ffa2d97533d4c100880e6936a6d1124bac751f
isatool unsymbolize;

diff -r f2ffa2d97533 -r 857688d775b0 NEWS
--- a/NEWS	Wed Jan 10 20:20:10 2001 +0100
+++ b/NEWS	Wed Jan 10 20:21:11 2001 +0100
@@ -47,6 +47,8 @@
 actual human-readable proof documents.  Please do not include goal
 states into document output unless you really know what you are doing!
 
+* isatool unsymbolize tunes sources for plain ASCII communication;
+
 
 *** Isar ***
 
diff -r f2ffa2d97533 -r 857688d775b0 doc-src/System/fonts.tex
--- a/doc-src/System/fonts.tex	Wed Jan 10 20:20:10 2001 +0100
+++ b/doc-src/System/fonts.tex	Wed Jan 10 20:21:11 2001 +0100
@@ -133,6 +133,23 @@
 \textsc{ascii}.  Thus users with \textsc{ascii}-only facilities will still be
 able to read your files.
 
+
+\section{Remove unreadable symbol names from sources --- \texttt{isatool unsymbolize}}
+
+The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
+readability for plain ASCII output (e.g.\ in mail communication).  Most
+notably, \texttt{unsymbolize} replaces arrow symbols such as
+\verb|\<Longrightarrow>| by \verb|==>|.
+\begin{ttbox}
+Usage: unsymbolize [FILES|DIRS...]
+
+  Recursively find .thy/.ML files, removing unreadable symbol names.
+  Note: this is an ad-hoc script; there is no systematic way to replace
+  symbols independently of the inner syntax of a theory!
+
+  Renames old versions of FILES by appending "~~".
+\end{ttbox}
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "system"