--- 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 ***
--- 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"