# HG changeset patch
# User oheimb
# Date 837197192 -7200
# Node ID 513316fd10873daf723aaebdf7aa3dd8deb31266
# Parent  cb1590accf3e912fb4872dd549c71de499d71367
*** empty log message ***

diff -r cb1590accf3e -r 513316fd1087 src/Tools/8bit/doc/manual.dvi
Binary file src/Tools/8bit/doc/manual.dvi has changed
diff -r cb1590accf3e -r 513316fd1087 src/Tools/8bit/doc/manual.itex
--- a/src/Tools/8bit/doc/manual.itex	Fri Jul 12 20:46:03 1996 +0200
+++ b/src/Tools/8bit/doc/manual.itex	Fri Jul 12 20:46:32 1996 +0200
@@ -23,7 +23,7 @@
 proofs in a quite pleasant form. 
 
 Instead of representing logical operators with ASCII character sequences, 
-a special graphical character font, resp. a \LaTeX{} 
+a special graphical character font, and alternatively a \LaTeX{} 
 command format, is provided. There are editors and a terminal
 capable of inputting and displaying the graphical characters, and converters
 between the different representations. The graphical font extends the normal
@@ -323,7 +323,7 @@
 
 \subsection{Preparations}
 
-To use the 8bit package, you have to set resp. extend the content of the 
+To use the 8bit package, you have to set respectively extend the content of the 
 following environment variables:
 
 \begin{itemize}
@@ -355,13 +355,14 @@
 
 \subsection{Installation and Configuration}
 
-To install the 8bit package, change directory to \bt{\$ISABELLE8BIT} and 
-run \bt{gmake} (the gnu version of \bt{make}) on the \bt{Makefile} there.
+To install the 8bit package, change directory to \bt{\$ISABELLE8BIT}.
+Configure the \bt{Makefile} there, then run \bt{gmake clean} 
+(\bt{gmake} is the gnu version of \bt{make}) and then \bt{gmake}.
 
 If you want to adapt the configuration of the font (keyboard bindings or
 conversion tables used by \bt{isa2latex}), change directory to\\
 \bt{\$ISABELLE8BIT/config} ,
-edit the files \bt{key-table.inp} resp. \bt{conv-tables.inp},
+edit the files \bt{key-table.inp} respectively \bt{conv-tables.inp},
 and run \bt{gmake} in this directory to generate new versions of 
 \bt{isa2latex}, editor support, and documentation.