src/Tools/8bit/man/man1/a2isa.1

use Args.mode;

.\" @(#)a2isa
.TH A2ISA 1 "23 May 1996" ""
.SH NAME
\fBa2isa\fP \- converts isabelle files, from ASCII to graphical characters

.IX a2isa#(1) "" "\fLa2isa\fP(1)"
.SH SYNOPSIS
.B a2isa
[\fIoptions\fP]

.SH DESCRIPTION
.B a2isa
converts the ASCII representation of special operators into graphical characters
(using the isabelle 8bit font). It is typically used to transform old isabelle
source files to new ones with graphical characters, which is desirable for
a more pleasant further editing and a safer translation to LaTeX format using
\fBisa2latex\fP. The translation of 
.B a2isa
is a bit smarter than the that of 
.B isa2latex
with the -A option set.
.B a2isa
normally reads its input from stdin and writes its output
to stdout.

Translations only take place inside strings, as this is the place inside 
treory and proof files where types, axioms and proof goals are formulated.
Many character sequences, such as "==>", can be translated quite safely, while
most single-character-operators like "|" are translated only if they are 
embedded in a preceding and successing space character. In special cases, the
output must be adapted manually.

\fIoptions\fP consists of one or a sequence of the following options:

.SH OPTIONS
.TP 5
.B "file" "\t"
read input from
.I file
instead of stdin

.TP 5
.B \-h "\t"
print a help message

.TP 5
.B \-o " file"
write output to
.I file
instead of stdout.
Note:
I/O redirection and "piping" are, of course, also possible.

.SH FILES
 8bit/bin/a2isa             (executable)
 8bit/c-sources/a2isa/lex.x (lex file containing
                             the translations used)

.SH RELATED COMMANDS
 isa2latex

.SH AUTHORS
 David von Oheimb