Initial revision
authoroheimb
Tue, 25 Jun 1996 17:44:43 +0200
changeset 1826 2a2c0dbeb4ac
parent 1825 88d4c33d7947
child 1827 724e7d8990ea
Initial revision
src/Tools/8bit/Makefile
src/Tools/8bit/README
src/Tools/8bit/axe/isaaxe
src/Tools/8bit/c-sources/a2isa/Makefile
src/Tools/8bit/c-sources/a2isa/a2isa
src/Tools/8bit/c-sources/a2isa/lex.x
src/Tools/8bit/c-sources/a2isa/main.c
src/Tools/8bit/c-sources/isa2latex/Makefile
src/Tools/8bit/c-sources/isa2latex/conv-defs.h
src/Tools/8bit/c-sources/isa2latex/conv-lex.x
src/Tools/8bit/c-sources/isa2latex/conv-main.c
src/Tools/8bit/c-sources/isa2latex/conv-tables.h
src/Tools/8bit/c-sources/isa2latex/conv-translate.c
src/Tools/8bit/c-sources/isa2latex/isa2latex
src/Tools/8bit/config/Makefile
src/Tools/8bit/config/README
src/Tools/8bit/config/conv-tables.inp
src/Tools/8bit/config/key-table.inp
src/Tools/8bit/doc/.Set2g.html
src/Tools/8bit/doc/.Set2g.thy.ML
src/Tools/8bit/doc/.Set2g_sub.html
src/Tools/8bit/doc/.Set2g_sup.html
src/Tools/8bit/doc/Makefile
src/Tools/8bit/doc/Set2.dvi
src/Tools/8bit/doc/Set2.tex
src/Tools/8bit/doc/Set2.thy
src/Tools/8bit/doc/Set2_a.thy
src/Tools/8bit/doc/Set2_g.thy
src/Tools/8bit/doc/Set2a.tex
src/Tools/8bit/doc/Set2g.thy
src/Tools/8bit/doc/Set2x.thy
src/Tools/8bit/doc/fkmatrix.dvi
src/Tools/8bit/doc/fkmatrix.tex
src/Tools/8bit/doc/fontindex.dvi
src/Tools/8bit/doc/fontindex.tex
src/Tools/8bit/doc/keyindex.dvi
src/Tools/8bit/doc/keyindex.tex
src/Tools/8bit/doc/manual.dvi
src/Tools/8bit/doc/manual.itex
src/Tools/8bit/doc/palette.isa
src/Tools/8bit/fonts/bash.inputrc
src/Tools/8bit/fonts/bdf-code.txt
src/Tools/8bit/fonts/fonts.dir
src/Tools/8bit/fonts/install
src/Tools/8bit/fonts/isacb24.bdf
src/Tools/8bit/fonts/isacr14.bdf
src/Tools/8bit/fonts/oldisacr14.bdf
src/Tools/8bit/fonts/spcb24.bdf
src/Tools/8bit/fonts/spcr14.bdf
src/Tools/8bit/gnu_emacs/.emacs_isa_gnu_emacs
src/Tools/8bit/gnu_emacs/goalify.el
src/Tools/8bit/gnu_emacs/isa_gnu_emacs
src/Tools/8bit/gnu_emacs/isa_gnu_emacs.emacs
src/Tools/8bit/isa-patches/HOL/HOL1.p
src/Tools/8bit/isa-patches/HOL/HOL2.p
src/Tools/8bit/isa-patches/HOL/Nat.p
src/Tools/8bit/isa-patches/HOL/Prod.p
src/Tools/8bit/isa-patches/HOL/Set.p
src/Tools/8bit/isa-patches/HOL/add-HOL.cfg
src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg
src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg
src/Tools/8bit/isa-patches/HOLCF/Cfun1.p
src/Tools/8bit/isa-patches/HOLCF/Cfun1.p2
src/Tools/8bit/isa-patches/HOLCF/Cprod3.p
src/Tools/8bit/isa-patches/HOLCF/HOLCF_ROOT.p
src/Tools/8bit/isa-patches/HOLCF/Holcfb.p
src/Tools/8bit/isa-patches/HOLCF/Lift3.p
src/Tools/8bit/isa-patches/HOLCF/Pcpo.p
src/Tools/8bit/isa-patches/HOLCF/Porder.p
src/Tools/8bit/isa-patches/HOLCF/Porder0.p
src/Tools/8bit/isa-patches/HOLCF/Sprod0.p
src/Tools/8bit/isa-patches/HOLCF/Sprod3.p
src/Tools/8bit/isa-patches/HOLCF/Ssum0.p
src/Tools/8bit/isa-patches/HOLCF/Ssum3.p
src/Tools/8bit/isa-patches/HOLCF/Tr1.p
src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg
src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg
src/Tools/8bit/keyboard/Linux/Xmodmap.linux
src/Tools/8bit/keyboard/Linux/Xmodmap.linux.doc
src/Tools/8bit/keyboard/Linux/Xresources.linux
src/Tools/8bit/keyboard/Linux/inputrc.linux
src/Tools/8bit/keyboard/Solaris/Xmodmap.solaris
src/Tools/8bit/keyboard/bash.inputrc
src/Tools/8bit/keyboard/install
src/Tools/8bit/latex/Set2a.tex
src/Tools/8bit/latex/isa2latex.sty
src/Tools/8bit/latex/supertab.sty
src/Tools/8bit/man/man1/a2isa.1
src/Tools/8bit/man/man1/gen-isa2latex.1
src/Tools/8bit/man/man1/gen-isadoc.1
src/Tools/8bit/man/man1/isa2latex.1
src/Tools/8bit/man/man1/isapal.1
src/Tools/8bit/man/man1/patcher.1
src/Tools/8bit/perl/codetable.pl
src/Tools/8bit/perl/generators/gen-isa2latex.pl
src/Tools/8bit/perl/generators/gen-isa_gnu_emacs.pl
src/Tools/8bit/perl/generators/gen-isa_xemacs.pl
src/Tools/8bit/perl/generators/gen-isaaxe.pl
src/Tools/8bit/perl/generators/gen-isadoc.pl
src/Tools/8bit/perl/generators/gen-isaterm.pl
src/Tools/8bit/perl/generators/gen-isavim.pl
src/Tools/8bit/perl/isapal.pl
src/Tools/8bit/perl/patcher.pl
src/Tools/8bit/perl/testperl.pl
src/Tools/8bit/term/initisaterm
src/Tools/8bit/term/isaterm
src/Tools/8bit/vim/initvim
src/Tools/8bit/vim/isavim
src/Tools/8bit/xemacs/isa_xemacs
src/Tools/8bit/xemacs/isa_xemacs.emacs
src/Tools/8bit/xmosaic/isa_xmosaic
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/Makefile	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,373 @@
+###############################################
+# Title:      Tools/8bit/Makefile
+# ID:         $Id$
+# Author:     Franz Regensburger
+# Copyright   1996 TU Muenchen
+#
+# Master Makefile for Isabelle 8bit package
+# ATTENTION: this is a GNU-MAKE Makefile
+#
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de>, 8.3.95
+# last changed:
+#	21.3.95	
+#	02.09.95 added latex2e support	
+#       07.02.96 added BASH variable and changed reference to amssym 
+#                in amssymb for latex2.09
+#       23.05.96 modifications by David von Oheimb
+#
+###############################################
+
+# operate silently
+MAKEFLAGS='s'
+
+###############################################
+# general configuration
+###############################################
+
+# path and name of bash shell
+# should be /bin/bash on every reasonable system 
+#
+#BASH=/bin/bash
+BASH=/bin/bash
+
+# Perl path and name for interpreter
+# should be a perl 4.x
+#PERL=/usr/bin/perl
+PERL=/usr/local/dist/DIR/perl4/bin/perl
+
+# use LaTeX2e instead of LaTeX 2.09
+# this flag is currently only sensible for perl script gen-isadoc
+# set to empty string for LaTeX 2.09
+#USE2E='-2e'
+USE2E='-2e'
+
+# name of GNU make utility: `make' on linux box; `gmake' on solaris
+#GMAKE=make
+GMAKE=gmake
+
+#keycode for Super_L       26 on SUN, 64  on Linux box 
+#SUPER_L=64
+SUPER_L=26
+
+#keycode for Hyper_R       20 on SUN, 113 on Linux box 
+#HYPER_R=113
+HYPER_R=20
+
+CONFIGFIlES = config/Makefile config/key-table.inp config/conv-tables.inp
+
+###############################################
+# configuration for configuration files in ./config
+###############################################
+
+CONV_SOURCE_DIR="$(ISABELLE8BIT)/c-sources/isa2latex"
+
+###############################################
+# configuration for GNU emacs
+###############################################
+
+# Name of your GNU emacs executable 
+GNU_ENAME=emacs
+
+#users init file ($HOME is added). This file is loaded after
+#the init file isa_gnu_emacs.emacs 
+GNU_INIT=.emacs_gnu_isa
+
+###############################################
+# configuration for xemacs
+###############################################
+
+# Name of your xemacs executable 
+
+XEMACS_ENAME=xemacs
+
+#users init file ($HOME is added). This file is loaded after
+#the init file isa_xemacs.emacs 
+
+XEMACS_INIT=.emacs_xemacs_isa
+
+###############################################
+# END of Configuration Section 
+###############################################
+
+
+###############################################
+# user targets        
+###############################################
+ 
+# ----------------------------------------------------
+
+# first target. Used if no target is given by the user
+#usage:
+#	echo "type 'make install' to install everything"
+#	echo "type 'make clean' to cleanup"
+
+# ----------------------------------------------------
+
+all:  $(CONFIGFIlES)\
+	bin/gen-isa2latex bin/gen-isaterm bin/gen-isavim bin/gen-isaaxe\
+	bin/gen-isa_gnu_emacs bin/gen-isa_xemacs bin/gen-isadoc\
+	configuration a2isa bin/isa2latex bin/a2isa\
+	bin/isa_gnu_emacs bin/isa_xemacs bin/isavim bin/isaaxe\
+	bin/isaterm bin/isa_xmosaic bin/isapal bin/codetable bin/patcher\
+	fonts/install keyboard/install\
+	manual
+
+# ----------------------------------------------------
+
+clean:
+	cd bin; rm -f *
+	cd c-sources/a2isa; $(GMAKE) clean
+	cd c-sources/isa2latex; $(GMAKE) clean
+	cd doc; rm -f *.log *.aux
+
+###############################################
+# internal targets        
+###############################################
+
+####### configuration files and the Makefile
+
+$(CONFIGFIlES): Makefile
+	@echo "configuring the configuration files"
+	@cd config;\
+	$(PERL) -pi \
+		-e "s#^USE2E\s*=.*#USE2E= $(USE2E)#g;" \
+		Makefile
+	@cd config;\
+	$(PERL) -pi \
+		-e "s#^BIN_DIR\s*\".*#BIN_DIR \"$(CONV_BIN_DIR)\"#g;" \
+		key-table.inp
+	@cd config;\
+	$(PERL) -pi \
+	-e "s#^CONV_SOURCE_DIR\s*\".*#CONV_SOURCE_DIR \"$(CONV_SOURCE_DIR)\"#g;" \
+	 conv-tables.inp
+
+#######      Generators        
+
+# ----------------------------------------------------
+	
+bin/gen-isa2latex: Makefile #perl/generators/gen-isa2latex.pl
+	@echo "configuring gen-isa2latex"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isa2latex.pl
+	@rm -f bin/gen-isa2latex;\
+	ln -s ../perl/generators/gen-isa2latex.pl bin/gen-isa2latex
+
+# ----------------------------------------------------
+	
+bin/gen-isaterm: Makefile #perl/generators/gen-isaterm.pl
+	@echo "configuring gen-isaterm"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isaterm.pl
+	@rm -f bin/gen-isaterm;\
+	ln -s ../perl/generators/gen-isaterm.pl bin/gen-isaterm
+
+# ----------------------------------------------------
+	
+bin/gen-isavim: Makefile #perl/generators/gen-isavim.pl
+	@echo "configuring gen-isavim"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isavim.pl
+	@rm -f bin/gen-isavim;\
+	ln -s ../perl/generators/gen-isavim.pl bin/gen-isavim
+
+# ----------------------------------------------------
+	
+bin/gen-isaaxe: Makefile #perl/generators/gen-isaaxe.pl
+	@echo "configuring gen-isaaxe"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isaaxe.pl
+	@rm -f bin/gen-isaaxe;\
+	ln -s ../perl/generators/gen-isaaxe.pl bin/gen-isaaxe
+
+# ----------------------------------------------------
+	
+bin/gen-isa_gnu_emacs: Makefile #perl/generators/gen-isa_gnu_emacs.pl
+	@echo "configuring gen-isa_gnu_emacs"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isa_gnu_emacs.pl
+	@rm -f bin/gen-isa_gnu_emacs;\
+	ln -s ../perl/generators/gen-isa_gnu_emacs.pl bin/gen-isa_gnu_emacs
+
+# ----------------------------------------------------
+	
+bin/gen-isa_xemacs: Makefile #perl/generators/gen-isa_xemacs.pl
+	@echo "configuring gen-isa_xemacs"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isa_xemacs.pl
+	@rm -f bin/gen-isa_xemacs;\
+	ln -s ../perl/generators/gen-isa_xemacs.pl bin/gen-isa_xemacs
+
+# ----------------------------------------------------
+	
+bin/gen-isadoc: Makefile #perl/generators/gen-isadoc.pl
+	@echo "configuring gen-isadoc"
+	@cd perl/generators;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		gen-isadoc.pl
+	@rm -f bin/gen-isadoc;\
+	ln -s ../perl/generators/gen-isadoc.pl bin/gen-isadoc
+
+
+#######      Converter        
+
+# ----------------------------------------------------
+	
+#isa2latex, editor support, font documentation:
+configuration:
+	@cd config; $(GMAKE)
+
+a2isa:
+	@cd c-sources/a2isa; $(GMAKE); $(GMAKE) clean
+
+bin/isa2latex: c-sources/isa2latex/isa2latex
+	@echo "installing isa2latex"
+	@rm -f bin/isa2latex;\
+	ln -s ../c-sources/isa2latex/isa2latex bin/isa2latex
+
+bin/a2isa: c-sources/a2isa/a2isa
+	@echo "installing a2isa"
+	@rm -f bin/a2isa;\
+	ln -s ../c-sources/a2isa/a2isa bin/a2isa
+
+#######      Editors        
+
+# ----------------------------------------------------
+	
+bin/isa_gnu_emacs: Makefile #gnu_emacs/isa_gnu_emacs
+	@echo "installing GNU emacs"
+	@cd gnu_emacs;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		-e "s#^ENAME\s*=.*#ENAME=$(GNU_ENAME)#g;"\
+		-e "s#^INIT\s*=.*#INIT=$(GNU_INIT)#g;" \
+		isa_gnu_emacs
+	@rm -f bin/isa_gnu_emacs;\
+	ln -s ../gnu_emacs/isa_gnu_emacs bin/isa_gnu_emacs
+
+# ----------------------------------------------------
+	
+bin/isa_xemacs: Makefile #xemacs/isa_xemacs
+	@echo "installing xemacs"
+	@@cd xemacs;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		-e "s#^ENAME\s*=.*#ENAME=$(XEMACS_ENAME)#g;"\
+		-e "s#^INIT\s*=.*#INIT=$(XEMACS_INIT)#g;" \
+		isa_xemacs
+	@rm -f bin/isa_xemacs;\
+	ln -s ../xemacs/isa_xemacs bin/isa_xemacs
+
+# ----------------------------------------------------
+	
+bin/isavim: Makefile #vim/isavim
+	@echo "installing vim"
+	@@cd vim;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		initvim ; \
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		isavim
+	@rm -f bin/isavim;\
+	ln -s ../vim/isavim bin/isavim
+
+# ----------------------------------------------------
+	
+bin/isaaxe: Makefile #axe/isaaxe
+	@echo "installing axe"
+	@cd axe;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		isaaxe
+	@rm -f bin/isaaxe;\
+	ln -s ../axe/isaaxe bin/isaaxe
+
+# ----------------------------------------------------
+	
+bin/isa_xmosaic: Makefile #xmosaic/isa_xmosaic
+	@echo "installing xmosaic"
+	@cd xmosaic;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		isa_xmosaic
+	@rm -f bin/isa_xmosaic;\
+	ln -s ../xmosaic/isa_xmosaic bin/isa_xmosaic
+
+#######      Terminal        
+
+# ----------------------------------------------------
+
+bin/isaterm: Makefile #term/isaterm
+	@echo "installing term"
+	@cd term;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		initisaterm;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		isaterm
+	@rm -f bin/isaterm;\
+	ln -s ../term/isaterm bin/isaterm	
+
+#######      other perl scripts
+
+# ----------------------------------------------------
+
+bin/isapal: Makefile #perl/isapal.pl
+	@echo "installing perl script isapal"
+	@cd perl;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;"\
+		isapal.pl
+	@rm -f bin/isapal;\
+	ln -s ../perl/isapal.pl bin/isapal
+
+bin/codetable: Makefile #perl/codetable.pl
+	@echo "installing perl script codetable"
+	@cd perl;\
+	$(PERL) -pi \
+		-e "s&^#!.*&#!$(PERL)&g;" \
+		codetable.pl
+	@rm -f bin/codetable;\
+	ln -s ../perl/codetable.pl bin/codetable
+
+bin/patcher: Makefile #perl/patcher.pl
+	@echo "installing perl script patcher"
+	@cd perl;\
+	$(PERL) -pi \
+	-e "s&^#!.*&#!$(PERL)&g;" \
+	patcher.pl
+	@rm -f bin/patcher;\
+	ln -s ../perl/patcher.pl bin/patcher
+
+fonts/install: Makefile
+	@cd fonts;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		install
+
+keyboard/install: Makefile
+	@cd keyboard;\
+	$(PERL) -pi\
+		-e "s&^#!.*&#!$(BASH)&g;" \
+		-e "s#^SUPER_L\s*=.*#SUPER_L=$(SUPER_L)#g;"\
+		-e "s#^HYPER_R\s*=.*#HYPER_R=$(HYPER_R)#g;"\
+		install
+
+# ----------------------------------------------------
+
+manual:
+	@cd doc; $(GMAKE) manual.dvi clean
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/README	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,147 @@
+See doc/manual.dvi for a full description of the 8bit package.
+
+
+USAGE of 8bit package:
+======================
+
+Configure or set the following environment variables:
+
+ISABELLE8BIT: set the directory of the isabelle 8bit package
+	e.g.:   /usr/proj/isabelle/src/Tools/8bit
+
+PATH: add the absolute path of the executables
+	e.g.:   $ISABELLE8BIT/bin
+
+MANPATH: add the absolute path of the manual pages
+	e.g.:   $ISABELLE8BIT/man
+
+TEXINPUTS: add the absolute path of special LaTeX style files used by the 8bit
+           package (if necessary)
+	e.g.:   $ISABELLE8BIT/latex: 
+
+
+
+INSTALLATION of 8bit package:
+==============================
+
+to install,
+	- change directory to $ISABELLE8BIT
+	- run gmake (the gnu version of make) on the Makefile there
+
+for adaptions of the configuration (in directory config/):
+	- configure the files: conv-tables.inp key-table.inp
+	- run gmake to generate isa2latex, editor support, and documentation
+
+for adapting the conversion table of a2isa (in directory c-sources/a2isa/):
+	- configure the file: lex.x
+	- run gmake there
+
+
+CONTENTS of the 8bit package distribution:
+==========================================
+
+directory axe/
+
+the files concerning isaaxe
+
+
+directory bin/
+
+available user commands concerning isabelle's graphical 8bit font:
+isa_xemacs	- replaces xemacs
+isa_gnu_emacs	- replaces emacs
+isaaxe		- replaces axe
+isavim		- replaces vim
+
+isaterm		- replaces xterm
+isapal		- shows the palette of available graphical characters
+codetable	- prints a the codes of all 8bit characters
+isa_xmosaic	- replaces xmosaic
+
+isa2latex	- converts a file with 8bit characters into a LaTeX source
+a2isa		- converts isabelle files, from ASCII to graphical characters
+
+gen-*		- for administration
+patcher		- for administration
+
+
+directory c-sources/a2isa/
+
+files concerning a2isa
+change lex.x to adapt its conversion table.
+
+
+directory c-sources/isa2latex/
+
+files concerning isa2latex
+change config/conv-tables.inp to adapt its conversion table.
+
+
+directory config/
+
+configuration files for keyboard input and the conversion table of isa2latex
+
+
+directory doc/
+
+manual.dvi	- manual of the 8bit package
+fontindex.dvi	- table of the 8bit characters, indexed by code
+keyindex.dvi	- table of the 8bit characters, indexed by input keystrokes
+fkmatrix.dvi	- table of the 8bit characters mapped to function keys
+
+directory fonts/
+font definitions for the Isabelle and Spectrum 8bit fonts
+install		- install the 8bit font
+
+directory keyboard/
+install		- set the keyboard modifiers
+subdirectories Solaris/ and Linux/ 
+		contain sample versions of useful .Xmodmap files
+
+directory gnu_emacs/
+
+files concerning isa_gnu_emacs
+
+
+directory isa-patches/ and subdirectories
+
+
+
+
+directory latex/
+
+isa2latex.sty	- Isabelle file style used by isa2latex
+
+directory man/man1/
+
+manual pages of some executables
+
+
+directory perl/
+
+simple perl scripts
+
+
+directory perl/generators/
+
+perl scripts for the configuration of many executables
+
+
+directory term/
+
+files concerning isaterm
+
+
+directory vim/
+
+files concerning isavim
+
+
+directory xemacs/
+
+files concerning isa_xemacs
+
+
+directory xmosaic/
+
+files concerning isa_xmosaic
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/axe/isaaxe	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,158 @@
+#!/bin/bash
+###############################################
+# Title:      Tools/8bit/axe/isaaxe
+# ID:         $Id$
+# Author:     Franz Regensburger
+# Copyright   1995 TU Muenchen
+#
+# open editor axe with isabelle font
+# derived from specaxe
+#
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 22.3.95
+# 
+###############################################
+#
+# This script opens the editor axe with the special 8bit font for Isabelle.
+# It also provides keyboard bindings for the access to the graphical characters.
+#
+# The script is configured by the master makefile ../Makefile and
+# the perl script ../bin/gen-isaaxe which reads the configuration file
+# ../config/key-table.inp. Edit these files to make changes!
+
+###############################################
+# do not edit below
+###############################################
+
+ISAAXEDIR=$ISABELLE8BIT/axe
+
+# make bash, axe, and vim accept 8 bit input 
+#export LANG=iso_8859_1
+export LESSCHARSET=latin1
+export INPUTRC=$ISABELLE8BIT/keyboard/bash.inputrc
+
+###############################################
+# Everything below and including the line
+# `*Axe*ed.translations: #override\'
+# is configured by the perl script `gen-isaaxe'. 
+#
+# DO NOT EDIT THE TRANSLATION MAP.
+#
+# In order to make changes to the keyboard mappings you should edit
+# the configuration file `../config/key-table.inp' which is interpreted by
+# the perl script `../bin/gen-isaaxe', 
+###############################################
+
+# start axe ; keyboard translations are given as resource string
+# the fonts can be selected with the font pulldown menu
+
+axe -fn "isacr14" -title "IsaAxe" -geometry 80x40 -xrm "\
+*fontMenu.label:    Fonts" -xrm "\
+*FontList: Isa14:isacr14 Isa24:isacb24" -xrm "\
+*Axe*ed.translations: #override\
+	!Mod2 Shift <Key>g:		insert-string(0xa1)  \n\
+	!Mod2 Shift <Key>d:		insert-string(0xa2)  \n\
+	!Mod2 Shift <Key>j:		insert-string(0xa3)  \n\
+	!Mod2 Shift <Key>l:		insert-string(0xa4)  \n\
+	!Mod2 Shift <Key>p:		insert-string(0xa5)  \n\
+	!Mod2 Shift <Key>s:		insert-string(0xa6)  \n\
+	!Mod2 Shift <Key>f:		insert-string(0xa7)  \n\
+	!Mod2 Shift <Key>q:		insert-string(0xa8)  \n\
+	!Mod2 Shift <Key>w:		insert-string(0xa9)  \n\
+	!Mod2 <Key>a:		insert-string(0xaa)  \n\
+	!Mod2 <Key>b:		insert-string(0xab)  \n\
+	!Mod2 <Key>g:		insert-string(0xac)  \n\
+	!Mod2 <Key>d:		insert-string(0xad)  \n\
+	!Mod2 <Key>e:		insert-string(0xae)  \n\
+	!Mod2 <Key>z:		insert-string(0xaf)  \n\
+	!Mod2 <Key>h:		insert-string(0xb0)  \n\
+	!Mod2 <Key>j:		insert-string(0xb1)  \n\
+	!Mod2 <Key>k:		insert-string(0xb2)  \n\
+	!Mod2 <Key>l:		insert-string(0xb3)  \n\
+	!Mod2 <Key>m:		insert-string(0xb4)  \n\
+	!Mod2 <Key>n:		insert-string(0xb5)  \n\
+	!Mod2 <Key>x:		insert-string(0xb6)  \n\
+	!Mod2 <Key>p:		insert-string(0xb7)  \n\
+	!Mod2 <Key>r:		insert-string(0xb8)  \n\
+	!Mod2 <Key>s:		insert-string(0xb9)  \n\
+	!Mod2 <Key>t:		insert-string(0xba)  \n\
+	!Mod2 <Key>f:		insert-string(0xbb)  \n\
+	!Mod2 <Key>c:		insert-string(0xbc)  \n\
+	!Mod2 <Key>q:		insert-string(0xbd)  \n\
+	!Mod2 <Key>w:		insert-string(0xbe)  \n\
+	!Mod4 <Key>n:		insert-string(0xbf)  \n\
+	!Mod4 <Key>a:		insert-string(0xc0)  \n\
+	!Mod4 <Key>o:		insert-string(0xc1)  \n\
+	!Mod4 <Key>f:		insert-string(0xc2)  \n\
+	!Mod4 <Key>t:		insert-string(0xc3)  \n\
+	!Mod4 Shift <Key>f:		insert-string(0xc4)  \n\
+	!Ctrl <Key>F5:		insert-string(0xc5)  \n\
+	!Ctrl <Key>F6:		insert-string(0xc6)  \n\
+	!Ctrl <Key>F7:		insert-string(0xc7)  \n\
+	!Ctrl <Key>F8:		insert-string(0xc8)  \n\
+	!Ctrl <Key>F9:		insert-string(0xc9)  \n\
+	!Ctrl <Key>F10:		insert-string(0xca)  \n\
+	!Ctrl <Key>F11:		insert-string(0xcb)  \n\
+	!Ctrl <Key>F12:		insert-string(0xcc)  \n\
+	!Mod4 <Key>F5:		insert-string(0xcf)  \n\
+	!Mod4 <Key>F6:		insert-string(0xf9)  \n\
+	!Mod4 <Key>F7:		insert-string(0xfa)  \n\
+	!Mod4 <Key>F1:		insert-string(0xd0)  \n\
+	!Mod4 <Key>F2:		insert-string(0xd1)  \n\
+	!Mod4 <Key>F3:		insert-string(0xd2)  \n\
+	!Mod4 <Key>F4:		insert-string(0xd3)  \n\
+	!Ctrl <Key>F1:		insert-string(0xd4)  \n\
+	!Ctrl <Key>F2:		insert-string(0xd5)  \n\
+	!Ctrl <Key>F3:		insert-string(0xd6)  \n\
+	!Ctrl <Key>F4:		insert-string(0xd7)  \n\
+	!Mod4 <Key>b:		insert-string(0xd8)  \n\
+	!Mod4 <Key>e:		insert-string(0xd9)  \n\
+	!Mod4 Shift <Key>e:		insert-string(0xda)  \n\
+	!Mod4 <Key>u:		insert-string(0xdb)  \n\
+	!Mod4 <Key>p:		insert-string(0xdc)  \n\
+	!Mod4 Shift <Key>p:		insert-string(0xdd)  \n\
+	!Mod4 <Key>l:		insert-string(0xde)  \n\
+	!Mod4 Shift <Key>l:		insert-string(0xdf)  \n\
+	!Mod4 <Key>g:		insert-string(0xe0)  \n\
+	!Mod4 Shift <Key>g:		insert-string(0xe1)  \n\
+	!Mod4 <Key>s:		insert-string(0xe2)  \n\
+	!Mod4 Shift <Key>s:		insert-string(0xe3)  \n\
+	!Shift <Key>F11:		insert-string(0xe4)  \n\
+	!Shift <Key>F12:		insert-string(0xe5)  \n\
+	!Mod2 <Key>F1:		insert-string(0xe6)  \n\
+	!Mod2 <Key>F2:		insert-string(0xe7)  \n\
+	!Mod2 <Key>F3:		insert-string(0xe8)  \n\
+	!Shift <Key>F1:		insert-string(0xe9)  \n\
+	!Shift <Key>F2:		insert-string(0xea)  \n\
+	!Shift <Key>F3:		insert-string(0xeb)  \n\
+	!Mod2 <Key>F5:		insert-string(0xec)  \n\
+	!Mod2 <Key>F6:		insert-string(0xed)  \n\
+	!Mod2 <Key>F7:		insert-string(0xee)  \n\
+	!Mod2 <Key>F8:		insert-string(0xef)  \n\
+	!Mod2 <Key>F9:		insert-string(0xf0)  \n\
+	!Mod2 <Key>F10:		insert-string(0xcd)  \n\
+	!Mod4 <Key>x:		insert-string(0xf2)  \n\
+	!Shift <Key>F5:		insert-string(0xf3)  \n\
+	!Shift <Key>F6:		insert-string(0xf4)  \n\
+	!Shift <Key>F7:		insert-string(0xf5)  \n\
+	!Shift <Key>F8:		insert-string(0xf6)  \n\
+	!Shift <Key>F9:		insert-string(0xf7)  \n\
+	!Shift <Key>F10:		insert-string(0xf8)  \n\
+	!Mod2 <Key>F11:		insert-string(0xce)  \n\
+	!Mod2 <Key>F12:		insert-string(0xf1)  \n\
+	!Mod4 <Key>F8:		insert-string(0xfb)  \n\
+	!Mod4 <Key>F9:		insert-string(0xfc)  \n\
+	!Mod4 <Key>F10:		insert-string(0xfd)  \n\
+	!Mod4 <Key>F11:		insert-string(0xfe)  \n\
+	!Mod4 <Key>F12:		insert-string(0xff)  \n\
+	!Shift <Key>F4:		insert-string(0xe9) insert-string(0xeb)  \n\
+	!Mod2 <Key>F4:		insert-string(0xe6) insert-string(0xe8)  \n\
+	!Mod4 <Key>i:		insert-string(0xe7) insert-string(0xe8)  \n\
+	!Mod4 Shift <Key>i:		insert-string(0xea) insert-string(0xeb)  \n\
+	!Mod4 <Key>m:		insert-string(0xe8)  \n\
+	!Mod4 Shift <Key>m:		insert-string(0xeb)  \n\
+	!Mod4 Shift <Key>n:		insert-string(0xf7)  \n\
+	! <Key>F9:		insert-string(0xc4)  \n\
+	! <Key>F10:		insert-string(0xea) insert-string(0xeb)  \n\
+	! <Key>F11:		insert-string(0xda)  \n\
+	! <Key>F12:		insert-string(0xdb)  \
+" $*
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/a2isa/Makefile	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,29 @@
+###############################################
+# Title:      Tools/8bit/c-sources/a2isa/Makefile
+# ID:         $Id$
+# Author:     David von Oheimb
+# Copyright   1996 TU Muenchen
+#
+# Makefile for Isabelle ASCII to 8bit converter
+################################################
+
+OBJECTS = main.o lex.o
+
+CC = gcc
+
+# Application name
+APPNAME = a2isa
+
+# ----------------------------------------------------
+
+$(APPNAME):  $(OBJECTS)
+	$(CC) -o $(APPNAME) $(OBJECTS);	strip $(APPNAME)
+
+lex.o: lex.x
+	flex lex.x; $(CC) -c -o lex.o lex.yy.c
+
+# ----------------------------------------------------
+
+clean:
+	@echo "     cleaning up object and tmp files..."
+	@rm -f *.o lex.yy.c
Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/a2isa/lex.x	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,178 @@
+/*  Title:      Tools/8bit/c-sources/a2isa/lex.x
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1996 TU Muenchen
+
+Isabelle ASCII to 8bit converter
+definitions for the lexical analyzer
+
+WARNING: the translations should be consistent with the configuration in
+         8bit/config/conv-tables.inp
+*/
+
+
+%{
+extern FILE *finput, *foutput;
+
+void put(char *s)
+{
+  while(*s)
+  {
+    fputc(*s++, yyout);
+  }
+}       
+%}
+
+%option 8bit
+%option yylineno
+%option noyywrap
+%x STRING
+
+%%
+  yyin  = finput;
+  yyout = foutput;
+
+\"			{ ECHO; BEGIN(STRING); }
+[^\"]*			{ ECHO; }
+<STRING>\"		{ ECHO; BEGIN(INITIAL); }
+<STRING>\\[ \t]*\n[ \t]*\\	{ ECHO; }
+<STRING>\n		{ ECHO; fprintf(stderr, 
+			  	"WARNING: line %d ends inside string\n", 
+				yylineno-1); }
+<STRING><<EOF>>		{ 	fprintf(stderr, 
+			  	"WARNING: EOF inside string\n"); 
+				yyterminate(); }
+
+<STRING>{
+   /* Pure */
+=>		put("");
+
+!!		put("");
+\[\|		put("");
+\|\]		put("");
+==>		put("");
+==		put("");
+
+   /* HOL */
+@		put("");
+\ &\ 		put("  ");
+\ \|\ 		put("  ");
+~\ 		put(" ");
+-->		put("");
+~=		put("");
+\%[ A-Za-z_]	{ *yytext=''; put(yytext); }
+EX!		put("!");
+\?!		put("!");
+EX\ 		put("");
+\?\ 		put("");
+ALL\ 		put("");
+![ A-Za-z_]	{ *yytext=''; put(yytext); }
+
+   /* Set */
+::		put("::");
+~:		put("");
+:		put("");
+  /*
+  > "{}"		"\mbox{$\emptyset$}"
+  > "<="		"\mbox{$\subseteq$}" 
+  */
+\ Int\ 		put("");
+\ Un\ 		put("");
+Inter\ 		put("");
+Union\ 		put("");
+
+   /* Nat */
+LEAST\ 		put("");
+
+   /* HOLCF */
+->		put("");
+\*\*		put("");
+\+\+		put("");
+
+\<\<		put("");
+  /*
+  > "<\|"		"\mbox{$<\!\mid$}"
+  > "<<\|"		"\mbox{$\ll\!\mid$}"
+  */
+LAM\ 		put("");
+lub\ 		put("");
+UU		put("");
+\(\|		put("");
+\|\)		put("");
+
+  /* misc */
+  /*
+  >  "\Gamma\ "		"\mbox{$\Gamma$}" 
+  >  "\Delta\ "		"\mbox{$\Delta$}" 
+  >  "\Theta\ "		"\mbox{$\Theta$}" 
+  >  "\Pi\ "		"\mbox{$\Pi$}" 
+  >  "\Sigma\ "		"\mbox{$\Sigma$}" 
+  >  "\Phi\ "		"\mbox{$\Phi$}" 
+  >  "\Psi\ "		"\mbox{$\Psi$}" 
+  >  "\Omega\ "		"\mbox{$\Omega$}" 
+
+  >  "\delta\ "		"\mbox{$\delta$}" 
+  >  "\epsilon\ "	"\mbox{$\varepsilon$}" 
+  >  "\zeta\ "		"\mbox{$\zeta$}" 
+  >  "\eta\ "		"\mbox{$\eta$}" 
+  >  "\theta\ "		"\mbox{$\vartheta$}" 
+  >  "\kappa\ "		"\mbox{$\kappa$}" 
+  >  "\mu\ "		"\mbox{$\mu$}" 
+  >  "\nu\ "		"\mbox{$\nu$}" 
+  >  "\xi\ "		"\mbox{$\xi$}" 
+  >  "\pi\ "		"\mbox{$\pi$}" 
+  >  "\phi\ "		"\mbox{$\varphi$}" 
+  >  "\chi\ "		"\mbox{$\chi$}" 
+  >  "\psi\ "		"\mbox{$\psi$}" 
+  >  "\omega\ "		"\mbox{$\omega$}" 
+
+  >  "\lceil\ "		"\mbox{$\lceil$}" 
+  >  "\rceil\ "		"\mbox{$\rceil$}" 
+  >  "\lfloor\ "		"\mbox{$\lfloor$}" 
+  >  "\rfloor\ "		"\mbox{$\rfloor$}" 
+  >  "\emptyset\ "	"\mbox{$\emptyset$}"
+  >  "\sqcap\ "		"\mbox{$\sqcap$}" 
+  >  "\sqcup\ "		"\mbox{$\sqcup$}" 
+  */
+
+glb\ 		put("");
+===		put("");
+
+  /*
+  >  "\sqsubset\ "	"\mbox{$\sqsubset$}" 
+  >  "\prec\ "		"\mbox{$\prec$}" 
+  >  "\preceq\ "	"\mbox{$\preceq$}" 
+  >  "\Succ\ "		"\mbox{$\succ$}" 
+  >  "\Succeq\ "	"\mbox{$\succeq$}" 
+  >  "\sim\ "		"\mbox{$\sim$}" 
+  >  "\simeq\ "		"\mbox{$\simeq$}" 
+  >  "\le\ "		"\mbox{$\le$}" 
+  >  "\ge\ "		"\mbox{$\ge$}" 
+  */
+
+\<==		put("");
+\<=>		put("");
+\<--		put("");
+\<->		put("");
+\<-		put("");
+
+  /*
+  >  "\mapsto\ "		"\mbox{$\mapsto$}" 
+  >  "\leadsto\ "	"\mbox{$\leadsto$}" 
+  >  "\uparrow\ "	"\mbox{$\uparrow$}" 
+  >  "\downarrow\ "	"\mbox{$\downarrow$}" 
+
+  >  "\ominus\ "		"\mbox{$\varominus$}" 
+  >  "\oslash\ "		"\mbox{$\varoslash$}" 
+  >  "\natural\ "	"\mbox{$\natural$}" 
+  >  "\infty\ "		"\mbox{$\infty$}" 
+  >  "\Box\ "		"\mbox{$\Box$}" 
+  >  "\Diamond\ "	"\mbox{$\Diamond$}" 
+  >  "\circ\ "		"\mbox{$\circ$}" 
+  >  "\bullet\ "		"\mbox{$\bullet$}" 
+  >  "||"		"\mbox{$\parallel$}" 
+  >  "\tick\ "		"\mbox{$\surd$}" 
+  >  "\filter\ "		"\mbox{\copyright}"
+  */
+}
+%%
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/a2isa/main.c	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,76 @@
+/*  Title:      Tools/8bit/c-sources/a2isa/main.c
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1996 TU Muenchen
+
+converter for isabelle files, from ASCII to graphical characters
+main file (ANSI-C)
+*/
+
+#include <stdio.h>
+
+extern int yylex(void);
+
+FILE* finput;                /* input file, default = stdin */
+FILE* foutput;               /* output file,default = stdout */
+
+void error(char* s, char* t)
+{
+  fprintf(stderr, "Error! %s: %s\n", s, t);
+}
+
+void usage(void)
+{
+  fprintf(stderr, "Isabelle ASCII to 8bit converter. Valid Options:\n");
+  fprintf(stderr, "<file>:    input file other than stdin\n");
+  fprintf(stderr, "-o <file>: output file other than stdout\n");
+  fprintf(stderr, "-h(elp):   print this message\n");
+}
+
+int main(int argc, char* argv[])
+{
+  char *s;                /* pointer to traverse components of argv */
+
+  finput = stdin;
+  foutput = stdout;
+
+  while (--argc > 0) {
+    s = *++argv;
+    if (*s++ == '-')
+      switch (*s) {
+        case 'h':
+          usage();
+          exit(0);
+        case 'o':
+          if (--argc) {
+            if ((foutput = fopen(*++argv, "w")) == NULL) {
+             error("Creating output file", *argv);
+              exit(-1);
+            }
+          } else {
+            error("No output file specified for option", s);
+            usage();
+            exit(-1);
+          }
+          break;
+        default:
+          error("Unknown option", s);
+          usage();
+          exit(-1);
+      } /* switch */
+    else
+      /*
+       * no further parameters with "-"; therefore we see input file:
+       */
+       if ((finput = fopen(--s, "r")) == NULL) {
+         error("Opening input file", s);
+         exit(-1);
+        }
+  }
+
+  yylex();
+
+  return(0);
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/Makefile	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,46 @@
+###############################################
+# Title:      Tools/8bit/c-sources/isa2latex/Makefile
+# ID:         $Id$
+# Author:     David von Oheimb
+# Copyright   1996 TU Muenchen
+#
+# Makefile for Isabelle converter
+# 30.3.92 by David von Oheimb
+# adjusted for isabelle converter: 22.2.95 by Franz Regensburger
+###############################################
+
+
+# Object files:
+OBJECTS = conv-main.o conv-lex.o conv-translate.o
+
+# Source files:
+SOURCES = conv-main.c conv-lex.x conv-translate.c
+
+# Compiler:
+CC = gcc
+
+# Application name
+APPNAME=isa2latex
+
+# ----------------------------------------------------
+
+$(APPNAME):   $(OBJECTS)
+	$(CC) -o $(APPNAME) $(OBJECTS); strip $(APPNAME)
+
+conv-main.o: conv-main.c conv-defs.h conv-tables.h
+	$(CC) -c conv-main.c
+
+conv-lex.o: conv-lex.x conv-defs.h conv-tables.h
+	flex -8 -t conv-lex.x | cat >tmp.c ; $(CC) -c -o conv-lex.o tmp.c
+
+#conv-lex.x:  ../../config/conv-tables.inp
+#	touch conv-lex.x
+
+conv-translate.o: conv-translate.c conv-defs.h
+	$(CC) -c conv-translate.c
+
+# ----------------------------------------------------
+
+clean:
+	@echo "     cleaning up object and tmp files..."
+	@rm -f *.o tmp.c tmp.txt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-defs.h	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,61 @@
+/*
+ * Definitions for the isabelle converster
+ */
+
+#define TRUE 1
+#define FALSE 0
+#define TAB 0x09
+
+/*
+ * Destination codes for translation; used for variable destCode
+ */
+
+#define TO_7bit   0
+#define TO_LaTeX  1
+#define DEFAULT_DEST TO_LaTeX
+
+/*
+ * Conversion modes: used for variable  convMode
+ */
+
+#define INCLUDE 1
+#define STANDALONE 2
+#define MIXED 3
+#define DEFAULT_MODE INCLUDE
+
+
+/*
+ * Number of tab positions in tabbing environment (see file isa2latex.sty)
+ */
+#define NUM_TABS 12
+
+/*
+ * character for tab definitions in LaTeX:
+ */
+#define NORMAL_TABBING_UNIT "x"
+#define BIG_TABBING_UNIT "g"
+
+/*
+ * units for tab used in tab calculations:
+ */
+#define TABBLANKS 8
+/* 
+   do not change below, the following definitions are automatically 
+   configured by the perl script gen-isa2latex
+*/
+
+/*
+ * Start and end index of translation tables
+ * LOW: ASCII characters with bit 8 unset
+ * HI:  ASCII characters with bit 8 set
+ * SEQ_TABLE: length of code table for long ASCII sequences 
+ */
+
+/* BEGIN gen-isa2latex */
+#define START_LOW_TABLE 32
+#define END_LOW_TABLE   126
+#define START_HI_TABLE  161
+#define END_HI_TABLE    255
+#define SEQ_TABLE       11
+/* END gen-isa2latex */
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,302 @@
+/*  Title:      Tools/8bit/c-sources/isa2latex/conv-main.c
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1996 TU Muenchen
+
+converter for isabelle files
+definitions for the lexical analyzer
+*/
+
+%{
+#include "conv-defs.h"
+#define output(c) fputc(c, yyout)
+#define BEGIN_ISA {	if (accept_ASCII)				\
+				BEGIN ISAA;	/* we have -A option */	\
+			else						\
+				BEGIN ISA;}
+
+extern FILE *finput, *foutput;
+extern int tabBlanks;
+extern int tabcount;
+extern char isa_env_beg[], isa_env_end[];
+extern int convMode;
+extern int accept_ASCII;
+extern int destCode;
+extern int cc;
+
+void reset_tabs(void);
+void put(char c, int longDetect, int longCode);
+
+int lineno=1;
+int inline_mode=FALSE;
+%}
+%S LATEX ISA ISAA ESC
+%option noyywrap
+
+%%
+  void warning(char *what);
+  void not_suitable(char *what, char *where);
+  yyin = finput;
+  yyout = foutput;
+
+  if (convMode == MIXED)
+	BEGIN LATEX;	/* we have -x option */
+  else 
+	BEGIN_ISA;
+
+<LATEX>\\I@		{ BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput, 
+				"{\\isainline{"); }
+<LATEX>\\I@isa[ \t]*\n?	{ BEGIN_ISA; inline_mode=FALSE; fprintf(foutput, 
+				isa_env_beg); reset_tabs(); 
+			  if (yytext[strlen(yytext)-1] == '\n') lineno++;
+			}
+<LATEX>\\E@		{ ECHO; not_suitable("\\E@","LATEX"); }
+<LATEX>\n		{ put(*yytext,FALSE,0); lineno++; }
+
+<ISA,ISAA>\\I@		{ if (inline_mode) 
+			  { BEGIN LATEX; inline_mode=FALSE; 
+			    fprintf(foutput, "}}"); }
+			  else
+			  { ECHO; not_suitable("\\I@","ISA"); }
+			}
+<ISA,ISAA>\n?[ \t]*\\I@isa	{ if (inline_mode)
+			  { ECHO; not_suitable("\\I@isa","INLINE"); }
+			  else
+			  { if (convMode == MIXED) {
+			      BEGIN LATEX; fprintf(foutput, isa_env_end); }
+			    else {
+			      ECHO; warning(
+				"\\I@isa only allowed with -x option"); }
+			  }
+			  if (yytext[0] == '\n') lineno++;
+			}
+<ISA,ISAA>\\E@		{ BEGIN ESC; fprintf(foutput, "{\\isaescape{"); }
+<ISA,ISAA><<EOF>>	{ if (convMode == MIXED) 
+			    not_suitable("EOF", inline_mode? "INLINE": "ISA");
+			   yyterminate(); 
+			}
+<ISA,ISAA>\n		{ if (inline_mode) 
+			  { ECHO; not_suitable("\\n","INLINE"); }
+			  else
+			  { put(*yytext,FALSE,0); }
+			  lineno++;
+			}
+<ISA,ISAA>\t		{ if (inline_mode)
+			  { ECHO; not_suitable("\\t","INLINE"); }
+			  else
+			  { put(*yytext,FALSE,0); }
+			}
+
+<ESC>\\I@		{ ECHO; not_suitable("\\I@"   ,"ESC"); }
+<ESC>\\I@isa		{ ECHO; not_suitable("\\I@isa","ESC"); }
+<ESC>\\E@		{ BEGIN_ISA; fprintf(foutput, "}}"); }
+<ESC><<EOF>>		{       not_suitable("EOF"    ,"ESC"); yyterminate(); }
+<ESC>\n			{ put(*yytext,FALSE,0); lineno++; }
+
+  /* The following is generated by the perl script gen-isa2latex. */
+  /* Make modifications in configuration file for gen-isa2latex!  */             
+  /* BEGIN_OF_HI_TABLE */
+<ISAA>\\Gamma\         	put((char)161,FALSE,0);
+<ISAA>\\Delta\         	put((char)162,FALSE,0);
+<ISAA>\\Theta\         	put((char)163,FALSE,0);
+<ISAA>LAM\             	put((char)164,FALSE,0);
+<ISAA>\\Pi\            	put((char)165,FALSE,0);
+<ISAA>\\Sigma\         	put((char)166,FALSE,0);
+<ISAA>\\Phi\           	put((char)167,FALSE,0);
+<ISAA>\\Psi\           	put((char)168,FALSE,0);
+<ISAA>\\Omega\         	put((char)169,FALSE,0);
+<ISAA>'a               	put((char)170,FALSE,0);
+<ISAA>'b               	put((char)171,FALSE,0);
+<ISAA>'c               	put((char)172,FALSE,0);
+<ISAA>\\delta\         	put((char)173,FALSE,0);
+<ISAA>\\varepsilon\    	put((char)174,FALSE,0);
+<ISAA>\\zeta\          	put((char)175,FALSE,0);
+<ISAA>\\eta\           	put((char)176,FALSE,0);
+<ISAA>\\vartheta\      	put((char)177,FALSE,0);
+<ISAA>\\kappa\         	put((char)178,FALSE,0);
+<ISAA>%\               	put((char)179,FALSE,0);
+<ISAA>\\mu\            	put((char)180,FALSE,0);
+<ISAA>\\nu\            	put((char)181,FALSE,0);
+<ISAA>\\xi\            	put((char)182,FALSE,0);
+<ISAA>\\pi\            	put((char)183,FALSE,0);
+<ISAA>'r               	put((char)184,FALSE,0);
+<ISAA>'s               	put((char)185,FALSE,0);
+<ISAA>'t               	put((char)186,FALSE,0);
+<ISAA>\\varphi\        	put((char)187,FALSE,0);
+<ISAA>\\chi\           	put((char)188,FALSE,0);
+<ISAA>\\psi\           	put((char)189,FALSE,0);
+<ISAA>\\omega\         	put((char)190,FALSE,0);
+<ISAA>~\               	put((char)191,FALSE,0);
+<ISAA>&\               	put((char)192,FALSE,0);
+<ISAA>\|\              	put((char)193,FALSE,0);
+<ISAA>!\               	put((char)194,FALSE,0);
+<ISAA>\?\              	put((char)195,FALSE,0);
+<ISAA>!!               	put((char)196,FALSE,0);
+<ISAA>\\lceil\         	put((char)197,FALSE,0);
+<ISAA>\\rceil\         	put((char)198,FALSE,0);
+<ISAA>\\lfloor\        	put((char)199,FALSE,0);
+<ISAA>\\rfloor\        	put((char)200,FALSE,0);
+<ISAA>\(\|             	put((char)201,FALSE,0);
+<ISAA>\|\)             	put((char)202,FALSE,0);
+<ISAA>\[\|             	put((char)203,FALSE,0);
+<ISAA>\|\]             	put((char)204,FALSE,0);
+<ISAA>{}               	put((char)205,FALSE,0);
+<ISAA>\ :\             	put((char)206,FALSE,0);
+<ISAA>\subseteq\       	put((char)207,FALSE,0);
+<ISAA>\ Int\           	put((char)208,FALSE,0);
+<ISAA>\ Un\            	put((char)209,FALSE,0);
+<ISAA>Inter\           	put((char)210,FALSE,0);
+<ISAA>Union\           	put((char)211,FALSE,0);
+<ISAA>\sqcap\          	put((char)212,FALSE,0);
+<ISAA>\sqcup\          	put((char)213,FALSE,0);
+<ISAA>glb\             	put((char)214,FALSE,0);
+<ISAA>lub\             	put((char)215,FALSE,0);
+<ISAA>UU               	put((char)216,FALSE,0);
+<ISAA>===              	put((char)217,FALSE,0);
+<ISAA>==               	put((char)218,FALSE,0);
+<ISAA>~=               	put((char)219,FALSE,0);
+<ISAA>\\sqsubset\      	put((char)220,FALSE,0);
+<ISAA><<               	put((char)221,FALSE,0);
+<ISAA>\\prec\          	put((char)222,FALSE,0);
+<ISAA>\\preceq\        	put((char)223,FALSE,0);
+<ISAA>\\succ\          	put((char)224,FALSE,0);
+<ISAA>\\succeq\        	put((char)225,FALSE,0);
+<ISAA>\\sim\           	put((char)226,FALSE,0);
+<ISAA>\\simeq\         	put((char)227,FALSE,0);
+<ISAA>\\le\            	put((char)228,FALSE,0);
+<ISAA>\\ge\            	put((char)229,FALSE,0);
+<ISAA><-               	put((char)230,FALSE,0);
+<ISAA>-@@@@@           	put((char)231,FALSE,0);
+<ISAA>->               	put((char)232,FALSE,0);
+<ISAA>\\Leftarrow\     	put((char)233,FALSE,0);
+<ISAA>=@@@@@           	put((char)234,FALSE,0);
+<ISAA>=>               	put((char)235,FALSE,0);
+<ISAA>->>              	put((char)236,FALSE,0);
+<ISAA>\\mapsto\        	put((char)237,FALSE,0);
+<ISAA>\\leadsto\       	put((char)238,FALSE,0);
+<ISAA>\\uparrow\       	put((char)239,FALSE,0);
+<ISAA>\\downarrow\     	put((char)240,FALSE,0);
+<ISAA>~:               	put((char)241,FALSE,0);
+<ISAA>\\times\         	put((char)242,FALSE,0);
+<ISAA>\\oplus\         	put((char)243,FALSE,0);
+<ISAA>\\ominus\        	put((char)244,FALSE,0);
+<ISAA>\\otimes\        	put((char)245,FALSE,0);
+<ISAA>\\oslash\        	put((char)246,FALSE,0);
+<ISAA>\\natural\       	put((char)247,FALSE,0);
+<ISAA>\\infty\         	put((char)248,FALSE,0);
+<ISAA>\\Box\           	put((char)249,FALSE,0);
+<ISAA>\\Diamond\       	put((char)250,FALSE,0);
+<ISAA>\\circ\          	put((char)251,FALSE,0);
+<ISAA>\\bullet\        	put((char)252,FALSE,0);
+<ISAA>\|\|             	put((char)253,FALSE,0);
+<ISAA>\\tick\          	put((char)254,FALSE,0);
+<ISAA>\\filter\        	put((char)255,FALSE,0);
+  /* END_OF_HI_TABLE */
+  /* This is the end of the generated part */
+
+  /* The following is generated by the perl script gen-isa2latex. */
+  /* Make modifications in configuration file for gen-isa2latex!  */             
+  /* BEGIN_OF_SEQ_TABLE */
+<ISA,ISAA>          	put((char)32,TRUE,0);
+<ISAA>==>         	put((char)32,TRUE,0);
+<ISA,ISAA>          	put((char)32,TRUE,1);
+<ISAA>-->         	put((char)32,TRUE,1);
+<ISA,ISAA>!          	put((char)32,TRUE,2);
+<ISAA>\?!         	put((char)32,TRUE,2);
+<ISA,ISAA>ALL@@@@@    	put((char)32,TRUE,3);
+<ISAA>ALL\        	put((char)32,TRUE,3);
+<ISA,ISAA>EX@@@@@     	put((char)32,TRUE,4);
+<ISAA>EX\         	put((char)32,TRUE,4);
+<ISA,ISAA><\|@@@@@    	put((char)32,TRUE,5);
+<ISAA><\|         	put((char)32,TRUE,5);
+<ISA,ISAA><<\|@@@@@   	put((char)32,TRUE,6);
+<ISAA><<\|        	put((char)32,TRUE,6);
+<ISA,ISAA>          	put((char)32,TRUE,7);
+<ISAA><==         	put((char)32,TRUE,7);
+<ISA,ISAA>          	put((char)32,TRUE,8);
+<ISAA><=>         	put((char)32,TRUE,8);
+<ISA,ISAA>          	put((char)32,TRUE,9);
+<ISAA><--         	put((char)32,TRUE,9);
+<ISA,ISAA>          	put((char)32,TRUE,10);
+<ISAA><->         	put((char)32,TRUE,10);
+  /* END_OF_SEQ_TABLE */
+  /* This is the end of the generated part */
+
+.			{ put(*yytext,FALSE,0);}
+
+%%
+
+void warning(char *str)
+{
+  fprintf(stderr,"WARNING: line %d: %s\n", lineno, str);
+}
+
+void not_suitable(char *what, char *where)
+{
+  char buf[80];
+  sprintf(buf, "'%s' inside %s mode", what, where);
+  warning(buf);
+}
+
+void reset_tabs(void)
+{
+  cc = 0;
+  tabcount = 1;
+}
+
+void put(char c, int longDetect,int longCode)
+{
+  int i;
+
+    if (YY_START == LATEX || YY_START == ESC)
+        /* do not translate in these modes */ 
+	fputc(c,foutput);
+
+    else /* we are in ISA mode */
+    if (longDetect) { /* lexer has scanned a long sequence */ 
+       fprintf(foutput, "%s", translateLong(longCode, destCode));
+        if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
+          tabcount++;
+       }
+    else /* lexer has not scanned a long sequence */		      
+    if (c & 0x80) { /* Hi-bit is set... */
+       fprintf(foutput, "%s", translateHi(c, destCode));
+        if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
+          tabcount++;
+    } 
+    else /* simple char without Hi-Bit*/
+    if (destCode == TO_7bit)
+        fputc(c, foutput);
+    else
+        switch (c) {  /* handle control codes */
+          case '\n': if (inline_mode)
+		       c=' ';
+		     else {
+		       fprintf(foutput, "\\\\\n");
+		       reset_tabs();
+		       break;
+		     }
+          case TAB:  if (inline_mode)
+		       c=' ';
+		     else {
+		       for (i = 0; i < tabcount; i++)
+		         fprintf(foutput, "\\>");
+		       reset_tabs();
+		       break;
+		     }
+         default:
+            if (++cc % tabBlanks == 0)
+              tabcount++;
+            if ((c >= START_LOW_TABLE) && (c <= END_LOW_TABLE))
+	      {
+              fprintf(foutput, "%s", translateLow(c));}
+            else /* just reproduce the other control codes */
+              fputc(c, foutput);
+        } /* switch */
+}       
+
+
+
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-main.c	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,249 @@
+/*  Title:      Tools/8bit/c-sources/isa2latex/conv-main.c
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1996 TU Muenchen
+
+converter for isabelle files
+main file (ANSI-C)
+
+   derived from
+
+      spec2latex: Version from 30.3.93
+      Authors  Franz Huber, B. Rumpe, David v. Oheimb 
+
+   New or changed features:
+
+     - flex is used to scan for multi character sequences
+     - automatic generation of flex source from user translation tables
+     - semantics of modes have changed, see the manpage 
+     - flag for latex2e
+*/         
+
+#include <stdio.h>
+
+/*
+ * VERSION:
+ */
+
+void version(void) {
+  fprintf(stderr, "Isabelle Converter, Version 1.4, 30 May 1996\n");
+}
+
+#include "conv-defs.h"
+#include "conv-tables.h"
+
+extern char *translateHi(int ch, int code);
+extern char *translateLow(int ch);
+extern char *translateLong(int ch);
+extern void reset_tabs(void);
+
+extern int yylex(void);
+
+FILE* finput;                /* input file, default = stdin */
+FILE* foutput;               /* output file,default = stdout */
+
+int use2e = FALSE;           /* generate latex2e output */
+int bigTabs = FALSE;         /* flag for big tabs */
+int tabBlanks = TABBLANKS;   /* number of blanks subsituted for a tab */
+char isa_env_beg[200];       /* latex command to begin isa environment */
+char isa_env_end[200];       /* latex command to end   isa environment */
+int cc;                      /* character counter in line  */
+int tabcount;                /* counter for tab positions  */
+
+int destCode = DEFAULT_DEST; /* default destination */
+int convMode = DEFAULT_MODE; /* default conversion mode  */
+int accept_ASCII = FALSE;    /* accept ASCII input for 8bit characters */
+
+/*
+ * einfache Fehlerbehandlung:
+ */
+ 
+void error(char* s, char* t) {
+  fprintf(stderr, "Error! %s: %s\n", s, t);
+}
+
+
+/*
+ * erklaert Programmbenutzung:
+ */
+ 
+void usage(void) {
+  fprintf(stderr, "Isabelle converter. Valid Options:\n");
+  fprintf(stderr, "<file>:    input file other than stdin\n");
+  fprintf(stderr, "-o <file>: output file other than stdout\n");
+  fprintf(stderr, "-a:        generate 7 bit ASCII representation\n");
+  fprintf(stderr, "-A:        accept ASCII representation of graphical characters (unsafe)\n");
+  fprintf(stderr, "-i:        generate LaTeX representation (default)\n");
+  fprintf(stderr, "           (for inclusion into other LaTeX documents)\n"); 
+  fprintf(stderr, "-s:        generate standalone LaTeX document\n");
+  fprintf(stderr, "-x:        allows mixture of specifications and given LaTeX parts\n");
+  fprintf(stderr, "-e:        generate LaTeX2e code (if option -s given)\n");
+  fprintf(stderr, "-t <num>:  set tabulator every <num> characters\n");
+  fprintf(stderr, "           (for conversion to LaTeX; default: 8)\n");
+  fprintf(stderr, "-b:        'BigTabs'; generates bigger tabbings\n");
+  fprintf(stderr, "           than standard for the LaTeX conversion\n");
+  fprintf(stderr, "-f <strg>: use another font than the default cmr-font when converting\n");
+  fprintf(stderr, "           to LaTeX. <strg> is the font-string in LaTeX syntax\n");
+  fprintf(stderr, "-v:        show version number and release date\n");
+  fprintf(stderr, "-h(elp):   print this message\n");
+}
+
+
+/*
+ * main programm
+ */
+
+int main(int argc, char* argv[]) {
+  char *s;                /* pointer to traverse components of argv */
+  char texFont[200];      /* string for TeX font change if destCode==TO_LaTeX */
+  int i,j;
+
+  /*
+   * initialize users font string:
+   */
+  texFont[0] = '\0';
+
+  finput = stdin;
+  foutput = stdout;
+
+  /*
+   * process command line
+   */
+  while (--argc > 0) {
+    s = *++argv;
+    if (*s++ == '-')
+      switch (*s) {
+        case 'v':
+          version();
+          exit(0);
+        case 'h':
+          usage();
+          exit(0);
+        case 'a':
+          destCode = TO_7bit;
+          break;
+        case 'A':
+          accept_ASCII = TRUE;
+          break;
+        case 'i':
+          destCode = TO_LaTeX;
+	  convMode = INCLUDE;
+          break;
+        case 's':
+          destCode = TO_LaTeX;
+	  convMode = STANDALONE;
+          break;
+        case 'x':
+          destCode = TO_LaTeX;
+	  convMode = MIXED;
+          break;
+        case 'e':
+          use2e = TRUE;
+          break;
+        case 'b':
+          bigTabs = TRUE;
+          break;
+        case 'f':
+          if (--argc)
+            strncpy(texFont, *++argv, 200);
+          else
+            error("No font specified with -f option, using default", s);
+          break;
+        case 'o':
+          if (--argc) {
+            if ((foutput = fopen(*++argv, "w")) == NULL) {
+             error("Creating output file", *argv);
+              exit(-1);
+            }
+          } else {
+            error("No output file specified for option", s);
+            usage();
+            exit(-1);
+          }
+          break;
+        case 't':
+          { int temp;
+            if (--argc) {
+              if (temp = atoi(*++argv))
+			    tabBlanks = temp;
+			  else {
+                error("Not a valid tabulator value", *argv);
+                exit(-1);
+              }
+            } else {
+              error("No value specified for option", s);
+              usage();
+              exit(-1);
+            }
+		  }
+          break;
+        default:
+          error("Unknown option", s);
+          usage();
+          exit(-1);
+      } /* switch */
+    else
+      /*
+       * no further parameters with "-"; therefore we see input file:
+       */
+       if ((finput = fopen(--s, "r")) == NULL) {
+         error("Opening input file", s);
+         exit(-1);
+        }
+  }
+
+  /*
+   * if destination is TO_LaTeX and mode is STANDALONE then produce LaTeX header
+   */
+  
+  if (convMode == STANDALONE) {
+    if (use2e){
+      fprintf(foutput, 
+	 "\\documentclass[a4paper,11pt]{article}\n");
+      fprintf(foutput, 
+	 "\\usepackage{latexsym,amssymb,isa2latex}\n");
+    } else {
+      fprintf(foutput, 
+	 "\\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}\n");
+    }
+      fprintf(foutput, "\\begin{document}\n");
+  }
+
+  if(texFont[0] != '\0') /* adjust font definition */
+    fprintf(foutput, "%s\n", texFont);
+
+  /*
+   * prepare a tabbing environment with tabstops every 'tabBlanks' blanks:
+   */
+  strcpy(isa_env_beg, "{\\isamode\\begin{tabbing}");
+  for (i = 0; i < NUM_TABS; i++) {
+    for (j = 0; j < tabBlanks; j++)
+      strcat(isa_env_beg, bigTabs ? BIG_TABBING_UNIT : NORMAL_TABBING_UNIT);
+    strcat(isa_env_beg, "\\=");
+  }
+  strcat(isa_env_beg, "\\kill{}\\hspace{-1ex}\n");
+  strcpy(isa_env_end, "\n\\end{tabbing}}");
+  
+  if (convMode == STANDALONE || convMode == INCLUDE)
+    fprintf(foutput, isa_env_beg);
+
+  /*
+   * start the conversion: use lexer in all modes to do the job.
+   */
+  
+  reset_tabs();
+  yylex();
+
+  /*
+   * output footers
+   */
+
+  if(convMode == STANDALONE || convMode == INCLUDE)
+    fprintf(foutput, isa_env_end);
+
+  if(convMode == STANDALONE) 
+      fprintf(foutput, "\\end{document}\n");
+  return(0);
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,253 @@
+/*
+ * translation table for the low-8-bit ascii codes
+ * translation takes place only if destCode is TO_LaTeX
+ *
+ * the row number + START_LOW_TABLE -1 is the ascii code !!
+ */
+
+/* do not edit the lines between BEGIN_OF_LOW_TABLE and END_OF_LOW_TABLE  */
+/* these lines are automatically generated by gen-isa2latex               */
+
+/* BEGIN_OF_LOW_TABLE */
+char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1] = {
+   "\\ ",
+   "!",
+   "\x22{}",
+   "\\#",
+   "\\$",
+   "\\%",
+   "\\mbox{$\\&$}",
+   "'",
+   "(",
+   ")",
+   "\\mbox{$*$}",
+   "\\mbox{$+$}",
+   ",",
+   "\\mbox{$-$}",
+   ".",
+   "/",
+   "0",
+   "1",
+   "2",
+   "3",
+   "4",
+   "5",
+   "6",
+   "7",
+   "8",
+   "9",
+   ":",
+   ";",
+   "\\mbox{$<$}",
+   "\\mbox{$=$}",
+   "\\mbox{$>$}",
+   "?",
+   "@",
+   "A",
+   "B",
+   "C",
+   "D",
+   "E",
+   "F",
+   "G",
+   "H",
+   "I",
+   "J",
+   "K",
+   "L",
+   "M",
+   "N",
+   "O",
+   "P",
+   "Q",
+   "R",
+   "S",
+   "T",
+   "U",
+   "V",
+   "W",
+   "X",
+   "Y",
+   "Z",
+   "\\mbox{$[$}",
+   "\\mbox{$\\backslash$}",
+   "\\mbox{$]$}",
+   "\\^{}",
+   "\\_",
+   "`",
+   "a",
+   "b",
+   "c",
+   "d",
+   "e",
+   "f",
+   "g",
+   "h",
+   "i",
+   "j",
+   "k",
+   "l",
+   "m",
+   "n",
+   "o",
+   "p",
+   "q",
+   "r",
+   "s",
+   "t",
+   "u",
+   "v",
+   "w",
+   "x",
+   "y",
+   "z",
+   "\\{",
+   "\\mbox{$|$}",
+   "\\}",
+   "\\~{}"
+};
+/* END_OF_LOW_TABLE */
+
+
+/*
+ * conversion table for Hi-8-bit table
+ *
+ * the row number + START_HIGH_TABLE -1 is the ascii code !!
+ * 
+ * first  column is used if destCode is TO_7bit
+ * second column is used if destCode is TO_LaTeX
+ */
+
+/* do not edit the lines between BEGIN_OF_HI_TABLE and END_OF_HI_TABLE  */
+/* these lines are automatically generated by gen-isa2latex             */
+
+/* BEGIN_OF_HI_TABLE */
+char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = {
+   {"\\Gamma"      ,"\\mbox{$\\Gamma$}"},
+   {"\\Delta"      ,"\\mbox{$\\Delta$}"},
+   {"\\Theta"      ,"\\mbox{$\\Theta$}"},
+   {"LAM"          ,"\\mbox{$\\Lambda$}"},
+   {"\\Pi"         ,"\\mbox{$\\Pi$}"},
+   {"\\Sigma"      ,"\\mbox{$\\Sigma$}"},
+   {"\\Phi"        ,"\\mbox{$\\Phi$}"},
+   {"\\Psi"        ,"\\mbox{$\\Psi$}"},
+   {"\\Omega"      ,"\\mbox{$\\Omega$}"},
+   {"'a"           ,"\\mbox{$\\alpha$}"},
+   {"'b"           ,"\\mbox{$\\beta$}"},
+   {"'c"           ,"\\mbox{$\\gamma$}"},
+   {"\\delta"      ,"\\mbox{$\\delta$}"},
+   {"\\varepsilon" ,"\\mbox{$\\varepsilon$}"},
+   {"\\zeta"       ,"\\mbox{$\\zeta$}"},
+   {"\\eta"        ,"\\mbox{$\\eta$}"},
+   {"\\vartheta"   ,"\\mbox{$\\vartheta$}"},
+   {"\\kappa"      ,"\\mbox{$\\kappa$}"},
+   {"%"            ,"\\mbox{$\\lambda$}"},
+   {"\\mu"         ,"\\mbox{$\\mu$}"},
+   {"\\nu"         ,"\\mbox{$\\nu$}"},
+   {"\\xi"         ,"\\mbox{$\\xi$}"},
+   {"\\pi"         ,"\\mbox{$\\pi$}"},
+   {"'r"           ,"\\mbox{$\\rho$}"},
+   {"'s"           ,"\\mbox{$\\sigma$}"},
+   {"'t"           ,"\\mbox{$\\tau$}"},
+   {"\\varphi"     ,"\\mbox{$\\varphi$}"},
+   {"\\chi"        ,"\\mbox{$\\chi$}"},
+   {"\\psi"        ,"\\mbox{$\\psi$}"},
+   {"\\omega"      ,"\\mbox{$\\omega$}"},
+   {"~"            ,"\\mbox{$\\neg$}"},
+   {"&"            ,"\\mbox{$\\wedge$}"},
+   {"|"            ,"\\mbox{$\\vee$}"},
+   {"!"            ,"\\mbox{$\\forall$}"},
+   {"?"            ,"\\mbox{$\\exists$}"},
+   {"!!"           ,"\\mbox{$\\bigwedge$}"},
+   {"\\lceil"      ,"\\mbox{$\\lceil$}"},
+   {"\\rceil"      ,"\\mbox{$\\rceil$}"},
+   {"\\lfloor"     ,"\\mbox{$\\lfloor$}"},
+   {"\\rfloor"     ,"\\mbox{$\\rfloor$}"},
+   {"(|"           ,"\\mbox{$(\\!|$}"},
+   {"|)"           ,"\\mbox{$|\\!)$}"},
+   {"[|"           ,"\\mbox{$[\\![$}"},
+   {"|]"           ,"\\mbox{$]\\!]$}"},
+   {"\\emptyset"   ,"\\mbox{$\\emptyset$}"},
+   {":"            ,"\\mbox{$\\in$}"},
+   {"\\subseteq"   ,"\\mbox{$\\subseteq$}"},
+   {"Int"          ,"\\mbox{$\\cap$}"},
+   {"Un"           ,"\\mbox{$\\cup$}"},
+   {"Inter"        ,"\\mbox{$\\bigcap$}"},
+   {"Union"        ,"\\mbox{$\\bigcup$}"},
+   {"\\sqcap"      ,"\\mbox{$\\sqcap$}"},
+   {"\\sqcup"      ,"\\mbox{$\\sqcup$}"},
+   {"glb"          ,"\\mbox{$\\overline{|\\,\\,|}$}"},
+   {"lub"          ,"\\mbox{$\\bigsqcup$}"},
+   {"UU"           ,"\\mbox{$\\perp$}"},
+   {"==="          ,"\\mbox{$\\doteq$}"},
+   {"=="           ,"\\mbox{$\\equiv$}"},
+   {"~="           ,"\\mbox{$\\not=$}"},
+   {"\\sqsubset"   ,"\\mbox{$\\sqsubset$}"},
+   {"<<"           ,"\\mbox{$\\sqsubseteq$}"},
+   {"\\prec"       ,"\\mbox{$\\prec$}"},
+   {"\\preceq"     ,"\\mbox{$\\preceq$}"},
+   {"\\succ"       ,"\\mbox{$\\succ$}"},
+   {"\\succeq"     ,"\\mbox{$\\succeq$}"},
+   {"\\sim"        ,"\\mbox{$\\sim$}"},
+   {"\\simeq"      ,"\\mbox{$\\simeq$}"},
+   {"\\le"         ,"\\mbox{$\\le$}"},
+   {"\\ge"         ,"\\mbox{$\\ge$}"},
+   {"<-"           ,"\\mbox{$\\leftarrow$}"},
+   {"-"            ,"\\mbox{$-$}"},
+   {"->"           ,"\\mbox{$\\rightarrow$}"},
+   {"<="           ,"\\mbox{$\\Leftarrow$}"},
+   {"="            ,"\\mbox{$=$}"},
+   {"=>"           ,"\\mbox{$\\Rightarrow$}"},
+   {"->>"          ,"\\mbox{$\\twoheadrightarrow$}"},
+   {"\\mapsto"     ,"\\mbox{$\\mapsto$}"},
+   {"\\leadsto"    ,"\\mbox{$\\leadsto$}"},
+   {"\\uparrow"    ,"\\mbox{$\\uparrow$}"},
+   {"\\downarrow"  ,"\\mbox{$\\downarrow$}"},
+   {"~:"           ,"\\mbox{$\\notin$}"},
+   {"*"            ,"\\mbox{$\\times$}"},
+   {"++"           ,"\\mbox{$\\oplus$}"},
+   {"\\ominus"     ,"\\mbox{$\\ominus$}"},
+   {"**"           ,"\\mbox{$\\otimes$}"},
+   {"\\oslash"     ,"\\mbox{$\\oslash$}"},
+   {"\\natural"    ,"\\mbox{$\\natural$}"},
+   {"\\infty"      ,"\\mbox{$\\infty$}"},
+   {"\\Box"        ,"\\mbox{$\\Box$}"},
+   {"\\Diamond"    ,"\\mbox{$\\Diamond$}"},
+   {"\\circ"       ,"\\mbox{$\\circ$}"},
+   {"\\bullet"     ,"\\mbox{$\\bullet$}"},
+   {"||"           ,"\\mbox{$\\parallel$}"},
+   {"\\tick"       ,"\\mbox{$\\surd$}"},
+   {"\\filter"     ,"\\mbox{\\copyright}"}
+};
+/* END_OF_HI_TABLE */
+
+
+/*
+ * conversion table for long ascii and 8bit sequences scanned by lexer
+ * 
+ * first  column is used if destCode is TO_7bit
+ * second column is used if destCode is TO_LaTeX
+ *
+ * Row - 1 is the code (longCode) used by the lexer
+ */      
+
+/* do not edit the lines between BEGIN_OF_SEQ_TABLE and END_OF_SEQ_TABLE  */
+/* these lines are automatically generated by gen-isa2latex               */
+
+/* BEGIN_OF_SEQ_TABLE */
+char *translationTableSeq[SEQ_TABLE][2] = {
+   {"==>"                        ,"\\mbox{$\\Longrightarrow$}"},
+   {"-->"                        ,"\\mbox{$\\longrightarrow$}"},
+   {"?!"                         ,"\\mbox{$\\exists$}!"},
+   {"ALL"                        ,"\\mbox{$\\forall$}"},
+   {"EX"                         ,"\\mbox{$\\exists$}"},
+   {"<|"                         ,"\\mbox{$<\\!\\mid$}"},
+   {"<<|"                        ,"\\mbox{$\\ll\\!\\mid$}"},
+   {"<=="                        ,"\\mbox{$\\Longleftarrow$}"},
+   {"<=>"                        ,"\\mbox{$\\Leftrightarrow$}"},
+   {"<--"                        ,"\\mbox{$\\longleftarrow$}"},
+   {"<->"                        ,"\\mbox{$\\leftrightarrow$}"}
+};
+/* END_OF_SEQ_TABLE */
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-translate.c	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,42 @@
+/*
+ * translation functions
+ * table ranges are checked
+ */
+
+
+#include <stdio.h>
+#include "conv-defs.h"
+
+extern char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1];
+extern char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2];
+extern char *translationTableSeq[SEQ_TABLE][2];
+
+char *translateLow(int ch) {
+  if ((ch >= START_LOW_TABLE) && (ch <= END_LOW_TABLE))
+    return (translationTableLow[ch - START_LOW_TABLE]);
+  else {
+    fprintf(stderr, "Error in translateLow!\n");
+	exit(-1);
+  }
+}
+
+char *translateHi(int ch, int code) { 
+  /*(256 + ch) is used to convert from character to unsigned short */ 
+  if (((256 + ch) >= START_HI_TABLE) && ((256 + ch) <= END_HI_TABLE))
+    return (translationTableHi[(256 + ch) - START_HI_TABLE][code]);
+  else {   
+    fprintf(stderr, "Sorry, the file contains a high-bit character which\n");
+    fprintf(stderr, "is not in the translation table!\n");
+    exit(-1);
+  }
+}
+
+char *translateLong(int ch, int code) {
+  if ((ch < SEQ_TABLE))
+    return (translationTableSeq[ch][code]);
+  else {
+    fprintf(stderr, "Error in translateLong!\n");
+	exit(-1);
+  }
+}
+
Binary file src/Tools/8bit/c-sources/isa2latex/isa2latex has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/Makefile	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,61 @@
+###############################################
+# Title:      Tools/8bit/config/Makefile
+# ID:         $Id$
+# Author:     Franz Regensburger
+# Copyright   1996 TU Muenchen
+#
+# Makefile for all the files that depend on the
+# configuration files 
+#	conv-tables.inp and key-table.inp 
+#
+# ATTENTION: this is a GNU-MAKE Makefile
+#
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 22.3.95
+###############################################
+
+# operate silently
+MAKEFLAGS='s'
+
+USE2E= '-2e'
+
+FONTDOCFILES = ../doc/fontindex.dvi ../doc/keyindex.dvi ../doc/fkmatrix.dvi
+# the dependent files
+FILES =  ../c-sources/isa2latex/conv-lex.x isa2latex\
+	../term/isaterm ../vim/isavim ../axe/isaaxe \
+	../gnu_emacs/isa_gnu_emacs.emacs ../xemacs/isa_xemacs.emacs \
+	$(FONTDOCFILES)
+
+precious: $(FILES)
+
+../c-sources/isa2latex/conv-lex.x: conv-tables.inp
+		@echo "generating isa2latex"
+		../bin/gen-isa2latex conv-tables.inp 
+
+isa2latex: 
+		@cd ../c-sources/isa2latex;\
+		gmake
+
+../term/isaterm: key-table.inp
+		@echo "generating isaterm"
+		../bin/gen-isaterm key-table.inp 
+
+../vim/isavim: key-table.inp
+		@echo "generating isavim"
+		../bin/gen-isavim key-table.inp 
+
+../axe/isaaxe: key-table.inp
+		@echo "generating isaaxe"
+		../bin/gen-isaaxe key-table.inp 
+	
+../gnu_emacs/isa_gnu_emacs.emacs: key-table.inp
+		@echo "generating isa_gnu_emacs"
+		../bin/gen-isa_gnu_emacs key-table.inp 
+
+../xemacs/isa_xemacs.emacs: key-table.inp
+		@echo "generating isa_xemacs"
+		../bin/gen-isa_xemacs key-table.inp 
+
+$(FONTDOCFILES): conv-tables.inp key-table.inp 
+		@echo "generating documentation"
+		../bin/gen-isadoc $(USE2E) conv-tables.inp key-table.inp 
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/README	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,10 @@
+Change configuration of translations and keyboard mappings:
+===========================================================
+
+If you change one of the the configuration files
+
+	key-table.inp
+	conv-tables.inp
+
+the Makefile updates all the files that depend on the configuration files.
+See the Makefile for the specific dependencies. 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/conv-tables.inp	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,412 @@
+############################################################
+# conv-tables.inp
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de>
+# 4.3.95
+# 
+# last edited
+# 11.3.95
+# 20-Mar-96 by David von Oheimb: SEQ_TABLE extended
+# 10-May-96 by David von Oheimb: HI_TABLE and SEQ_TABLE rearranged
+#
+#
+############################################################
+#
+# This is the configuration file for the converter isa2latex
+# It is interpreted by the perl script `gen-isa2latex' which
+# produces rsp. changes the followong files of the converter
+# sources:
+#
+#  Makefile, conv-tables.h, conv-defs.h and conv-lex.x
+#
+# In the perl script, regular expressions are used to identify
+# the keywords. In order to be sure that something is treated
+# as a comment, simply begin the line with a # sign. This is
+# fool proof.
+#
+############################################################ 
+
+############################################################ 
+# General setup
+#
+### Absolut path to the sources of the converter, 
+#   Must be readable for user.
+#   
+#   Must be delimited by "
+#
+
+CONV_SOURCE_DIR "/usr/proj/isabelle/8bit/c-sources/isa2latex"
+
+# End of  general setup
+############################################################ 
+
+############################################################ 
+# Setup for translationTableLow in file conv-tables.h
+#
+
+### Start index START_LOW_TABLE of translationTableLow
+#   The index END_LOW_TABLE is computed from the length
+#   of the translation  table LOW_TABLE below.
+#
+#   constraints: 32 <= START_LOW_TABLE <= 127 
+#                START_LOW_TABLE + length(LOW_TABLE) - 1 <= 127 
+#
+#   Must be delimited by "
+#
+
+START_LOW_TABLE "32"
+
+### The translation table LOW_TABLE
+#
+#   Keyword for the begin of the table is BEGIN_LOW_TABLE
+#   Keyword for the end of the table is   END_LOW_TABLE
+#
+#   Lines beginning with # are ignored as everywhere in this file.
+#   Lines obeying the syntax given below are treated as table entries.
+#   All other lines are ignored, too. This is for comments.
+#
+#   Syntax of a table entry:
+#   
+#   > "LaTeX replacement"  anything
+#
+#   The double quotes enclose the LaTeX replacement in pure 
+#   LaTeX syntax. 
+#   Every \ in the string except when used for hex-notation \x?? is
+#   automatically duplicated by the script! The strings are used in
+#   printf output statements in the C code.
+#
+#   Attention: you have to use hex-notation \x22 to produce a " inside 
+#   the double quoted strings. An explicit " will terminate the string.
+#
+#   The following `anything' is ignored by the perl script.
+#   This is for comments.
+#   
+#   The ordering of entries in the table LOW_TABLE is relevant!
+#   Empty table is not allowed.
+#
+#
+
+BEGIN_LOW_TABLE
+>  "\ "			Blank 
+>  "!"
+#
+# if you don't like double quotes to be removed insert the following
+#>  "\\x22{}"		double quotes are not removed 
+>  "\x22{}"		double quotes are not removed 
+#
+>  "\#"
+>  "\$"
+>  "\%"
+>  "\mbox{$\&$}"
+>  "'"
+>  "("
+>  ")"
+>  "\mbox{$*$}"
+>  "\mbox{$+$}"
+>  ","
+>  "\mbox{$-$}"
+>  "."
+>  "/"
+>  "0"
+>  "1"
+>  "2"
+>  "3"
+>  "4"
+>  "5"
+>  "6"
+>  "7"
+>  "8"
+>  "9"
+>  ":"
+>  ";"
+>  "\mbox{$<$}"
+>  "\mbox{$=$}"
+>  "\mbox{$>$}"
+>  "?"
+>  "@"
+>  "A"
+>  "B"
+>  "C"
+>  "D"
+>  "E"
+>  "F"
+>  "G"
+>  "H"
+>  "I"
+>  "J"
+>  "K"
+>  "L"
+>  "M"
+>  "N"
+>  "O"
+>  "P"
+>  "Q"
+>  "R"
+>  "S"
+>  "T"
+>  "U"
+>  "V"
+>  "W"
+>  "X"
+>  "Y"
+>  "Z"
+>  "\mbox{$[$}"
+>  "\mbox{$\backslash$}"	Backslash
+>  "\mbox{$]$}"
+>  "\^{}"			
+>  "\_"	
+>  "`"
+>  "a"
+>  "b"
+>  "c"
+>  "d"
+>  "e"
+>  "f"
+>  "g"
+>  "h"
+>  "i"
+>  "j"
+>  "k"
+>  "l"
+>  "m"
+>  "n"
+>  "o"
+>  "p"
+>  "q"
+>  "r"
+>  "s"
+>  "t"
+>  "u"
+>  "v"
+>  "w"
+>  "x"
+>  "y"
+>  "z"
+>  "\{"
+>  "\mbox{$|$}"
+>  "\}"
+>  "\~{}"	negation
+END_LOW_TABLE
+
+############################################################ 
+# Setup for translationTableHi in file conv-tables.h
+#
+
+### Start index START_HI_TABLE of translationTableHi
+#   The index END_HI_TABLE is computed from the length
+#   of the translation table HI_TABLE below.
+#
+#   constraints: 128 <= START_HI_TABLE <= 255
+#                START_HI_TABLE + length(HI_TABLE) - 1 <= 255 
+#                
+#
+#   Must be delimited by "
+#
+
+START_HI_TABLE "161"
+
+### The translation table HI_TABLE
+#
+#   Keyword for the begin of the table is BEGIN_HI_TABLE
+#   Keyword for the end of the table is   END_HI_TABLE
+#
+#   Lines beginning with # are ignored as everywhere in this file.
+#   Lines obeying the syntax given below are treated as table entries.
+#   All other lines are ignored, too. This is for comments.
+#
+#   Syntax of a table entry:
+#   
+#   > "lex expression ascii" "ascii replacement" "LaTeX replacement"  anything
+#
+#   The double quotes enclose the lex expression, the ascii replacement, and the
+#   LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. 
+#
+#   The string for the lex expression is literally passed to lex. Backslashes
+#   are not duplicated!
+#   Every \ in the replacements except when used for hex-notation \x?? is
+#   automatically duplicated by the script! The strings are used in
+#   printf output statements in the C code.
+#
+#   Attention: you have to use hex-notation \x22 to produce a " inside 
+#   the double quoted strings. An explicit " will terminate the string.
+#
+#   The following `anything' is ignored by the perl script.
+#   This is for comments.
+#
+#   The ordering of entries in the table HI_TABLE is relevant!
+#   Empty table is not allowed.
+#
+#
+
+BEGIN_HI_TABLE
+
+# big greek letters
+>  "\\Gamma\ "		"\Gamma"	"\mbox{$\Gamma$}" 
+>  "\\Delta\ "		"\Delta"	"\mbox{$\Delta$}" 
+>  "\\Theta\ "		"\Theta"	"\mbox{$\Theta$}" 
+>  "LAM\ "		"LAM"		"\mbox{$\Lambda$}" 
+>  "\\Pi\ "		"\Pi"		"\mbox{$\Pi$}" 
+>  "\\Sigma\ "		"\Sigma"	"\mbox{$\Sigma$}" 
+>  "\\Phi\ "		"\Phi"		"\mbox{$\Phi$}" 
+>  "\\Psi\ "		"\Psi"		"\mbox{$\Psi$}" 
+>  "\\Omega\ "		"\Omega"	"\mbox{$\Omega$}" 
+
+# small greek letters, HOL, HOLCF
+>  "'a"			"'a"		"\mbox{$\alpha$}" 
+>  "'b"			"'b"		"\mbox{$\beta$}" 
+>  "'c"			"'c"		"\mbox{$\gamma$}" 
+>  "\\delta\ "		"\delta"	"\mbox{$\delta$}" 
+>  "\\varepsilon\ "	"\varepsilon"	"\mbox{$\varepsilon$}" 
+>  "\\zeta\ "		"\zeta"		"\mbox{$\zeta$}" 
+>  "\\eta\ "		"\eta"		"\mbox{$\eta$}" 
+>  "\\vartheta\ "	"\vartheta"	"\mbox{$\vartheta$}" 
+>  "\\kappa\ "		"\kappa"	"\mbox{$\kappa$}" 
+>  "%\ "		"%"		"\mbox{$\lambda$}" 
+>  "\\mu\ "		"\mu"		"\mbox{$\mu$}" 
+>  "\\nu\ "		"\nu"		"\mbox{$\nu$}" 
+>  "\\xi\ "		"\xi"		"\mbox{$\xi$}" 
+>  "\\pi\ "		"\pi"		"\mbox{$\pi$}" 
+>  "'r"			"'r"		"\mbox{$\rho$}" 
+>  "'s"			"'s"		"\mbox{$\sigma$}" 
+>  "'t"			"'t"		"\mbox{$\tau$}" 
+>  "\\varphi\ "		"\varphi"	"\mbox{$\varphi$}" 
+>  "\\chi\ "		"\chi"		"\mbox{$\chi$}" 
+>  "\\psi\ "		"\psi"		"\mbox{$\psi$}" 
+>  "\\omega\ "		"\omega"	"\mbox{$\omega$}" 
+
+# logical symbols, HOL
+>  "~\ "		"~"		"\mbox{$\neg$}" 
+>  "&\ "		"&"		"\mbox{$\wedge$}" 
+>  "\|\ "		"|"		"\mbox{$\vee$}" 
+>  "!\ "		"!"		"\mbox{$\forall$}" 
+>  "\?\ "		"?"		"\mbox{$\exists$}"
+>  "!!"			"!!"		"\mbox{$\bigwedge$}" 
+
+# parenthesis. Pure, HOLCF
+>  "\\lceil\ "		"\lceil"	"\mbox{$\lceil$}" 
+>  "\\rceil\ "		"\rceil"	"\mbox{$\rceil$}" 
+>  "\\lfloor\ "		"\lfloor"	"\mbox{$\lfloor$}" 
+>  "\\rfloor\ "		"\rfloor"	"\mbox{$\rfloor$}" 
+>  "\(\|"		"(|"		"\mbox{$(\!|$}"		#\llparenthesis
+>  "\|\)"		"|)"		"\mbox{$|\!)$}"		#\rrparenthesis
+>  "\[\|"		"[|"		"\mbox{$[\![$}"		#\llbracket
+>  "\|\]"		"|]"		"\mbox{$]\!]$}"		#\rrbracket
+
+# set theory, HOL
+>  "{}"			"\emptyset"	"\mbox{$\emptyset$}"
+>  "\ :\ "		":"		"\mbox{$\in$}" 
+>  "\subseteq\ "	"\subseteq"	"\mbox{$\subseteq$}" 
+>  "\ Int\ "		"Int"		"\mbox{$\cap$}" 
+>  "\ Un\ "		"Un"		"\mbox{$\cup$}" 
+>  "Inter\ "		"Inter"		"\mbox{$\bigcap$}" 
+>  "Union\ "		"Union"		"\mbox{$\bigcup$}" 
+
+# domain theory, HOLCF
+>  "\sqcap\ "		"\sqcap"	"\mbox{$\sqcap$}" 
+>  "\sqcup\ "		"\sqcup"	"\mbox{$\sqcup$}" 
+>  "glb\ "		"glb"		"\mbox{$\overline{|\,\,|}$}" #\bigsqcap
+>  "lub\ "		"lub"		"\mbox{$\bigsqcup$}" 
+>  "UU"			"UU"		"\mbox{$\perp$}" 
+
+# relational symbols, Pure, HOLCF
+>  "==="		"==="		"\mbox{$\doteq$}" 
+>  "=="			"=="		"\mbox{$\equiv$}" 
+>  "~="			"~="		"\mbox{$\not=$}" 
+>  "\\sqsubset\ "	"\sqsubset"	"\mbox{$\sqsubset$}" 
+>  "<<"			"<<"		"\mbox{$\sqsubseteq$}" 
+>  "\\prec\ "		"\prec"		"\mbox{$\prec$}" 
+>  "\\preceq\ "		"\preceq"	"\mbox{$\preceq$}" 
+>  "\\succ\ "		"\succ"		"\mbox{$\succ$}" 
+>  "\\succeq\ "		"\succeq"	"\mbox{$\succeq$}" 
+>  "\\sim\ "		"\sim"		"\mbox{$\sim$}" 
+>  "\\simeq\ "		"\simeq"	"\mbox{$\simeq$}" 
+>  "\\le\ "		"\le"		"\mbox{$\le$}" 
+>  "\\ge\ "		"\ge"		"\mbox{$\ge$}" 
+
+# arrows, Pure, HOL
+>  "<-"		"<-"		"\mbox{$\leftarrow$}" 
+>  "-@@@@@"		"-"		"\mbox{$-$}" 
+>  "->"			"->"		"\mbox{$\rightarrow$}" 
+>  "\\Leftarrow\ "	"<="		"\mbox{$\Leftarrow$}" 
+>  "=@@@@@"		"="		"\mbox{$=$}" 
+>  "=>"			"=>"		"\mbox{$\Rightarrow$}" 
+>  "->>"		"->>"		"\mbox{$\twoheadrightarrow$}" 
+>  "\\mapsto\ "		"\mapsto"	"\mbox{$\mapsto$}" 
+>  "\\leadsto\ "	"\leadsto"	"\mbox{$\leadsto$}" 
+>  "\\uparrow\ "	"\uparrow"	"\mbox{$\uparrow$}" 
+>  "\\downarrow\ "	"\downarrow"	"\mbox{$\downarrow$}" 
+>  "~:"			"~:"		"\mbox{$\notin$}" 
+
+# arithmetic, HOLCF
+>  "\\times\ "		"*"		"\mbox{$\times$}" 
+>  "\\oplus\ "		"++"		"\mbox{$\oplus$}"	#\varoplus
+>  "\\ominus\ "		"\ominus"	"\mbox{$\ominus$}" "	#\varominus
+>  "\\otimes\ "		"**"		"\mbox{$\otimes$}" "	#\varotimes
+>  "\\oslash\ "		"\oslash"	"\mbox{$\oslash$}" 	#\varoslash
+>  "\\natural\ "	"\natural"	"\mbox{$\natural$}" 
+>  "\\infty\ "		"\infty"	"\mbox{$\infty$}" 
+
+# misc
+>  "\\Box\ "		"\Box"		"\mbox{$\Box$}" 
+>  "\\Diamond\ "	"\Diamond"	"\mbox{$\Diamond$}" 
+>  "\\circ\ "		"\circ"		"\mbox{$\circ$}" 
+>  "\\bullet\ "		"\bullet"	"\mbox{$\bullet$}" 
+>  "\|\|"		"||"		"\mbox{$\parallel$}" 
+>  "\\tick\ "		"\tick"		"\mbox{$\surd$}" 
+>  "\\filter\ "		"\filter"	"\mbox{\copyright}"
+END_HI_TABLE
+
+############################################################ 
+# Setup for translationTableSeq in file conv-tables.h
+# and lexer source conv-lex.x
+# 
+#   Keyword for the being of the table is BEGIN_SEQ_TABLE
+#   Keyword for the end of the table is   END_SEQ_TABLE
+#
+#   Lines beginning with # are ignored as everywhere in this file.
+#   Lines obeying the syntax given below are treated as table entries.
+#   All other lines are ignored, too. This is for comments.
+#
+#   Syntax of a table entry:
+#   
+#   > "lex expr 8bit" "lex expr ascii" "ascii replace" "LaTeX replace" anything
+#
+#   The double quotes enclose the lex expressions, the ascii replacement, and
+#   the  LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. 
+#   
+#   The strings for the lex expressions are literally passed to lex. Backslashes
+#   are not duplicated!
+#   Every \ in the replacements except when used for hex-notation \x?? is
+#   automatically duplicated by the script! The strings are used in
+#   printf output statements in the C code.
+#
+#   Attention: you have to use hex-notation \x22 to produce a " inside 
+#   the double quoted strings. An explicit " will terminate the string.
+#
+#   The following `anything' is ignored by the perl script.
+#   This is for comments.
+#
+#   The ordering of entries in table SEQ_TABLE is irrelevant!
+#   Empty table is allowed.
+#
+
+BEGIN_SEQ_TABLE
+
+# Pure
+>  ""		"==>"		"==>"		"\mbox{$\Longrightarrow$}"
+
+# HOL
+>  ""		"-->"		"-->"		"\mbox{$\longrightarrow$}"
+>  "!"		"\?!"		"?!"		"\mbox{$\exists$}!"
+>  "ALL@@@@@"	"ALL\ "		"ALL"		"\mbox{$\forall$}" 
+>  "EX@@@@@"	"EX\ "		"EX"		"\mbox{$\exists$}" 
+
+#HOLCF
+>  "<\|@@@@@"	"<\|"		"<|"		"\mbox{$<\!\mid$}"
+>  "<<\|@@@@@"	"<<\|"		"<<|"		"\mbox{$\ll\!\mid$}"
+
+# misc ?
+>  ""		"<=="		"<=="		"\mbox{$\Longleftarrow$}"
+>  ""		"<=>"		"<=>"		"\mbox{$\Leftrightarrow$}"
+>  ""		"<--"		"<--"		"\mbox{$\longleftarrow$}"
+>  ""		"<->"		"<->"		"\mbox{$\leftrightarrow$}"
+END_SEQ_TABLE
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/key-table.inp	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,186 @@
+############################################################
+# key-tables.inp
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de>
+# 21.3.95
+# 
+# last edited
+# 
+#
+############################################################
+#
+# This is the configuration file for the keyboard mappings
+# which is used by various scripts of the 8-bit package.
+# It is interpreted by several perl scripts.
+#
+# In the perl script, regular expressions are used to identify
+# the keywords. In order to be sure that something is treated
+# as a comment, simply begin the line with a # sign. This is
+# fool proof.
+#
+############################################################ 
+
+############################################################ 
+# General setup
+#
+### Absolut path to the 8-bit package, 
+#   Must be delimited by "
+#
+
+### Directory, where the links to various scripts reside.
+#   
+#   Must be delimited by "
+#
+
+BIN_DIR ""
+
+### Subdirectories where the sources of various scripts reside and
+#   where the configured scripts will be put.
+#
+#   The entries must be delimited by "
+#
+
+
+GNU_EMACS_DIR "gnu_emacs"
+XEMACS_DIR "xemacs"
+
+AXE_DIR "axe"
+VIM_DIR "vim"
+TERM_DIR "term"
+DOC_DIR "doc"
+
+# End of  general setup
+############################################################ 
+
+############################################################ 
+# Setup for the keymap
+#
+# each configuration line has the form
+# MOD mod KEY key CODESEQ codeseq
+# 
+# MOD, KEY and CODE are keywords
+#
+# The emacses are the reason for the restrictions below!
+#
+#     mod: THE modifier used (no modifier sequences).
+#	   known modifiers are Mod1, Mod2, Mod4, Shift, Ctrl and None for
+#          for NO modifier :-)  
+#
+#     key: allowed keys are a-z, A-Z and the function keys F0 - F99.
+#          uppercase letters A-Z are translated to Shift + lowercase for the
+#          xmodmap based tools.   
+#
+#    code: a comma seperated list of twodigit hex-numbers. 
+#          write `af' for \xaf and `af, ae' for the sequence \xaf,\xae 
+#
+# The table must be delimited by BEGIN_KEY_MAP and END_KEY_MAP
+
+BEGIN_KEY_MAP
+	MOD Mod2	KEY G		CODE a1
+	MOD Mod2	KEY D		CODE a2
+	MOD Mod2	KEY J		CODE a3
+	MOD Mod2	KEY L		CODE a4
+	MOD Mod2	KEY P		CODE a5
+	MOD Mod2	KEY S		CODE a6
+	MOD Mod2	KEY F		CODE a7
+	MOD Mod2	KEY Q		CODE a8
+	MOD Mod2	KEY W		CODE a9
+	MOD Mod2	KEY a		CODE aa
+	MOD Mod2	KEY b		CODE ab
+	MOD Mod2	KEY g		CODE ac
+ 	MOD Mod2	KEY d		CODE ad
+	MOD Mod2	KEY e		CODE ae
+	MOD Mod2	KEY z		CODE af
+	MOD Mod2	KEY h		CODE b0
+	MOD Mod2	KEY j		CODE b1
+	MOD Mod2	KEY k		CODE b2
+	MOD Mod2	KEY l		CODE b3
+	MOD Mod2	KEY m		CODE b4
+	MOD Mod2	KEY n		CODE b5
+	MOD Mod2	KEY x		CODE b6
+	MOD Mod2	KEY p		CODE b7
+	MOD Mod2	KEY r		CODE b8
+	MOD Mod2	KEY s		CODE b9
+	MOD Mod2	KEY t		CODE ba
+	MOD Mod2	KEY f		CODE bb
+	MOD Mod2	KEY c		CODE bc
+	MOD Mod2	KEY q		CODE bd
+	MOD Mod2	KEY w		CODE be
+	MOD Mod4	KEY n		CODE bf
+	MOD Mod4	KEY a		CODE c0
+	MOD Mod4	KEY o		CODE c1
+	MOD Mod4	KEY f		CODE c2
+	MOD Mod4	KEY t		CODE c3
+	MOD Mod4	KEY F		CODE c4
+	MOD Ctrl	KEY F5		CODE c5
+	MOD Ctrl	KEY F6		CODE c6
+	MOD Ctrl	KEY F7		CODE c7
+	MOD Ctrl	KEY F8		CODE c8
+	MOD Ctrl	KEY F9		CODE c9
+	MOD Ctrl	KEY F10		CODE ca
+	MOD Ctrl	KEY F11		CODE cb
+	MOD Ctrl	KEY F12		CODE cc
+	MOD Mod4	KEY F5		CODE cf
+	MOD Mod4	KEY F6		CODE f9
+	MOD Mod4	KEY F7		CODE fa
+	MOD Mod4	KEY F1		CODE d0
+	MOD Mod4	KEY F2		CODE d1
+	MOD Mod4	KEY F3		CODE d2
+	MOD Mod4	KEY F4		CODE d3
+	MOD Ctrl	KEY F1		CODE d4
+	MOD Ctrl	KEY F2		CODE d5
+	MOD Ctrl	KEY F3		CODE d6
+	MOD Ctrl	KEY F4		CODE d7
+	MOD Mod4	KEY b		CODE d8
+	MOD Mod4	KEY e		CODE d9
+	MOD Mod4	KEY E		CODE da
+	MOD Mod4	KEY u		CODE db
+	MOD Mod4	KEY p		CODE dc
+	MOD Mod4	KEY P		CODE dd
+	MOD Mod4	KEY l		CODE de
+	MOD Mod4	KEY L		CODE df
+	MOD Mod4	KEY g		CODE e0
+	MOD Mod4	KEY G		CODE e1
+	MOD Mod4	KEY s		CODE e2
+	MOD Mod4	KEY S		CODE e3
+	MOD Shift	KEY F11		CODE e4
+	MOD Shift	KEY F12		CODE e5
+	MOD Mod2	KEY F1		CODE e6
+	MOD Mod2	KEY F2		CODE e7
+	MOD Mod2	KEY F3		CODE e8
+	MOD Shift	KEY F1		CODE e9
+	MOD Shift	KEY F2		CODE ea
+	MOD Shift	KEY F3		CODE eb
+	MOD Mod2	KEY F5		CODE ec
+	MOD Mod2	KEY F6		CODE ed
+	MOD Mod2	KEY F7		CODE ee
+	MOD Mod2	KEY F8		CODE ef
+	MOD Mod2	KEY F9		CODE f0
+	MOD Mod2	KEY F10		CODE cd
+	MOD Mod4	KEY x		CODE f2
+	MOD Shift	KEY F5		CODE f3
+	MOD Shift	KEY F6		CODE f4
+	MOD Shift	KEY F7		CODE f5
+	MOD Shift	KEY F8		CODE f6
+	MOD Shift	KEY F9		CODE f7
+	MOD Shift	KEY F10		CODE f8
+	MOD Mod2	KEY F11		CODE ce
+	MOD Mod2	KEY F12		CODE f1
+	MOD Mod4	KEY F8		CODE fb
+	MOD Mod4	KEY F9		CODE fc
+	MOD Mod4	KEY F10		CODE fd
+	MOD Mod4	KEY F11		CODE fe
+	MOD Mod4	KEY F12		CODE ff
+	MOD Shift	KEY F4		CODE e9,eb
+	MOD Mod2	KEY F4		CODE e6,e8
+	MOD Mod4	KEY i		CODE e7,e8
+	MOD Mod4	KEY I		CODE ea,eb
+	MOD Mod4	KEY m		CODE e8
+	MOD Mod4	KEY M		CODE eb
+	MOD Mod4	KEY N		CODE f7
+	MOD None	KEY F9		CODE c4
+	MOD None	KEY F10		CODE ea,eb
+	MOD None	KEY F11		CODE da
+	MOD None	KEY F12		CODE db
+END_KEY_MAP
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g.html	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,27 @@
+<HTML><HEAD><TITLE>Set2g.thy</TITLE></HEAD>
+
+<BODY>
+<H2>Set2g.thy</H2>
+<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
+<HR>
+
+<PRE>
+Set2g = <A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord.html">Ord</A> +
+
+types
+	'a set
+consts
+	Ball	:: "'a set  ('a  bool)  bool"
+syntax
+	"GBall"	:: "pttrn  'a set  bool  bool"	("(3__./ _)" 10)
+translations
+(*		"xA. P" == "Ball A (x. P)"*)
+		"GBall x A P" == "Ball A (x. P)"
+
+(*defs
+
+     Ball_def	"Ball A P  x. xA  P(x)"
+*)
+end
+</PRE>
+<HR></BODY></HTML>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g.thy.ML	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,43 @@
+val thy = mk_base [Thy "Ord"] "Set2g" true;
+
+structure Set2g =
+struct
+
+local
+ val parse_ast_translation = [];
+ val parse_translation = [];
+ val print_translation = [];
+ val print_ast_translation = [];
+in
+
+
+
+val thy = thy
+
+|> add_trfuns
+(parse_ast_translation, parse_translation, print_translation, print_ast_translation)
+
+|> add_types
+[("set", 1, NoSyn)]
+
+|> add_tyabbrs
+[]
+
+|> add_consts
+[("Ball", "'a set  ('a  bool)  bool", NoSyn)]
+
+|> add_syntax
+[("GBall", "pttrn  'a set  bool  bool", Mixfix ("(3 _  _ ./ _)", [], 10))]
+
+|> add_trrules
+[("logic", " x  A . P") <-> ("logic", "Ball A (x. P)")]
+
+|> add_thyname "Set2g";
+
+val _ = store_theory (thy, "Set2g");
+
+
+
+
+end;
+end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g_sub.html	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+<HTML><HEAD><TITLE>Children of Set2g</TITLE></HEAD>
+<H2>Children of theory Set2g</H2>
+The name of every theory is linked to its theory file<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A> stands for subtheories (child theories)<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A> stands for supertheories (parent theories)
+<P>
+<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
+<HR>
+<PRE><A HREF=".Set2g.html">Set2g</A> <A HREF = ".Set2g_sup.html"><IMG SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" BORDER=0 ALT = \/></A>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g_sup.html	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,13 @@
+<HTML><HEAD><TITLE>Ancestors of Set2g</TITLE></HEAD>
+<H2>Ancestors of theory Set2g</H2>
+The name of every theory is linked to its theory file<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A> stands for subtheories (child theories)<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A> stands for supertheories (parent theories)
+<BR><TT>...</TT> stands for repeated subtrees<P>
+<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
+<HR>
+<PRE><A HREF=".Set2g.html">Set2g</A> <A HREF = ".Set2g_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A>
+ \__<A HREF="../../../../stud/oheimb/isabelle/HOL/.Ord.html">Ord</A> <A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A><A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord_sup.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A>
+     \__<A HREF="../../../../stud/oheimb/isabelle/HOL/.HOL.html">HOL</A> <A HREF = "../../../../stud/oheimb/isabelle/HOL/.HOL_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A><A HREF = "../../../../stud/oheimb/isabelle/HOL/.HOL_sup.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A>
+         \__CPure <A HREF = "../../../../stud/oheimb/isabelle/HOL/.CPure_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A>
+</PRE><HR></BODY></HTML>
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Makefile	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,36 @@
+###############################################
+# Title:      Tools/8bit/doc/Makefile
+# ID:         $Id$
+# Author:     David von Oheimb
+# Copyright   1996 TU Muenchen
+#
+# Makefile for the document files
+###############################################
+
+# operate silently
+MAKEFLAGS='s'
+
+LATEX=latex
+ISA2LATEX=isa2latex
+
+CHECKOUT=co
+
+.SUFFIXES: $(SUFFIXES) .itex .thy .ML .tex .dvi
+
+.itex.tex:
+	$(ISA2LATEX) -x -e -o $@ $<
+.thy.tex .ML.tex:
+	$(ISA2LATEX) -s -e -f '\oddsidemargin-1cm{}\evensidemargin-1cm' -o $@ $<
+.tex.dvi:
+	$(LATEX) $<
+
+FONTDOCFILES = fontindex.dvi keyindex.dvi fkmatrix.dvi
+
+fontdocfiles: $(FONTDOCFILES)
+
+manual: manual.tex manual.dvi
+
+manual.tex: manual.itex
+
+clean:
+	rm -f *.aux *.log
Binary file src/Tools/8bit/doc/Set2.dvi has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2.tex	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,17 @@
+\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}
+\begin{document}
+{\isamode
+\begin{tabbing}
+xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex}
+consts\\
+\>Ball\>::\ "\mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ (\mbox{$\alpha$}\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"\\
+syntax\\
+\>"@Ball"\>::\ "pttrn\ \mbox{$\Rightarrow$}\ \mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"\>\>\>\>\>("(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"\ 10)\\
+translations\\
+\>\>"\mbox{$\forall$}x\mbox{$\in$}A.\ P"\ \mbox{$\equiv$}\ "Ball\ A\ (\mbox{$\lambda$}x.\ P)"\\
+defs\\
+\ \ \ \ \ Ball\_def\>\>"Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"\\
+\\
+
+\end{tabbing}}
+\end{document}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2.thy	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+	Ball	:: "'a set => ('a => bool) => bool"
+syntax
+	"@Ball"	:: "pttrn => 'a set => bool => bool"	("(3!_:_./ _)" 10)
+translations
+		"!x:A. P" == "Ball A (%x. P)"
+defs
+     Ball_def	"Ball A P == !x. x:A --> P x"
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2_a.thy	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+	Ball	:: "'a set => ('a => bool) => bool"
+syntax
+	"@Ball"	:: "pttrn => 'a set => bool => bool"	("(3! _ : _./ _)" 10)
+translations
+		"! x : A. P" == "Ball A (% x. P)"
+defs
+     Ball_def	"Ball A P == ! x. x : A --> P x"
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2_g.thy	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+	Ball	:: "'a set  ('a  bool)  bool"
+syntax
+	"Ball"	:: "pttrn  'a set  bool  bool"	("(3__./ _)" 10)
+translations
+		"xA. P" == "Ball A (x. P)"
+defs
+     Ball_def	"Ball A P  x. xA  P x"
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2a.tex	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,17 @@
+\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}
+\begin{document}
+{\isamode
+\begin{tabbing}
+xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex}
+consts\\
+\>Ball\>::\ "{}'a\ set\ \mbox{$\Rightarrow$}\ ('a\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"{}\\
+syntax\\
+\>"{}\mbox{$\varepsilon$}Ball"{}\>::\ "{}pttrn\ \mbox{$\Rightarrow$}\ 'a\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"{}\>\>\>\>\>("{}(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"{}\ 10)\\
+translations\\
+\>\>"{}\mbox{$\forall$}x\mbox{$\in$}A.\ P"{}\ \mbox{$=$}\mbox{$=$}\ "{}Ball\ A\ (\mbox{$\lambda$}x.\ P)"{}\\
+defs\\
+\ \ \ \ \ Ball\_def\>\>"{}Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"{}\\
+\\
+
+\end{tabbing}}
+\end{document}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2g.thy	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+	Ball	:: "'a set  ('a  bool)  bool"
+syntax
+	"GBall"	:: "pttrn  'a set  bool  bool"	("(3__./ _)" 10)
+translations
+		"xA. P" == "Ball A (x. P)"
+defs
+     Ball_def	"Ball A P  x. xA  P x"
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2x.thy	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+	Ball	:: "'a set  ('a  bool)  bool"
+syntax
+	"Ball"	:: "pttrn  'a set  bool  bool"	("(3!__./ _)" 10)
+translations
+		"xA. P" == "Ball A (x. P)"
+defs
+     Ball_def	"Ball A P   x. xA  P x"
+
Binary file src/Tools/8bit/doc/fkmatrix.dvi has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/fkmatrix.tex	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,32 @@
+\documentclass[a4paper,11pt]{article}
+\usepackage{latexsym,latexsym,amssymb,supertab}
+
+\begin{document}
+
+\begin{center}
+{\Large 
+  Keyboard Mapping for Function Keys F1 - F12}\\ 
+  Date: \today 
+
+\vspace*{.5cm}
+
+\tablehead{\hline
+Modifier & F1 &F2 &F3 &F4 &F5 &F6 &F7 &F8 &F9 & F10 &F11 &F12\\
+\hline}
+\tabletail{\hline}
+
+\begin{supertabular}{|l|l|l|l|l|l|l|l|l|l|l|l|l|}
+None& & & & & & & & &\mbox{$\bigwedge$}&\mbox{$\Longrightarrow$}&\mbox{$\equiv$}&\mbox{$\not=$}\nextline
+\hline
+Shift&\mbox{$\Leftarrow$}&\mbox{$=$}&\mbox{$\Rightarrow$}&\mbox{$\Leftrightarrow$}&\mbox{$\oplus$}&\mbox{$\ominus$}&\mbox{$\otimes$}&\mbox{$\oslash$}&\mbox{$\natural$}&\mbox{$\infty$}&\mbox{$\le$}&\mbox{$\ge$}\nextline
+\hline
+Alt&\mbox{$\leftarrow$}&\mbox{$-$}&\mbox{$\rightarrow$}&\mbox{$\leftrightarrow$}&\mbox{$\twoheadrightarrow$}&\mbox{$\mapsto$}&\mbox{$\leadsto$}&\mbox{$\uparrow$}&\mbox{$\downarrow$}&\mbox{$\emptyset$}&\mbox{$\in$}&\mbox{$\notin$}\nextline
+\hline
+AltGraph&\mbox{$\cap$}&\mbox{$\cup$}&\mbox{$\bigcap$}&\mbox{$\bigcup$}&\mbox{$\subseteq$}&\mbox{$\Box$}&\mbox{$\Diamond$}&\mbox{$\circ$}&\mbox{$\bullet$}&\mbox{$\parallel$}&\mbox{$\surd$}&\mbox{\copyright}\nextline
+\hline
+Ctrl&\mbox{$\sqcap$}&\mbox{$\sqcup$}&\mbox{$\overline{|\,\,|}$}&\mbox{$\bigsqcup$}&\mbox{$\lceil$}&\mbox{$\rceil$}&\mbox{$\lfloor$}&\mbox{$\rfloor$}&\mbox{$(\!|$}&\mbox{$|\!)$}&\mbox{$[\![$}&\mbox{$]\!]$}\\
+\hline
+Meta& & & & & & & & & & & & \nextline
+\end{supertabular}
+\end{center}
+\end{document}
Binary file src/Tools/8bit/doc/fontindex.dvi has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/fontindex.tex	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,117 @@
+\documentclass[a4paper,11pt]{article}
+\usepackage{latexsym,amssymb,supertab}
+
+\begin{document}
+
+\begin{center}
+{\Large 
+  Description of Isabelle Font \\ 
+      Indexed by Code}\\
+  Date: \today 
+
+\vspace*{.5cm}
+
+\tablehead{\hline
+Oct & Dec & Hex & ASCII & \LaTeX & Key Sequence\\
+\hline}
+\tabletail{\hline}
+
+\begin{supertabular}{|l|l|l|l|l|l|}
+241 & 161 & a1 & \verb*"\Gamma" & \mbox{$\Gamma$} & Alt G\nextline
+242 & 162 & a2 & \verb*"\Delta" & \mbox{$\Delta$} & Alt D\nextline
+243 & 163 & a3 & \verb*"\Theta" & \mbox{$\Theta$} & Alt J\nextline
+244 & 164 & a4 & \verb*"LAM" & \mbox{$\Lambda$} & Alt L\nextline
+245 & 165 & a5 & \verb*"\Pi" & \mbox{$\Pi$} & Alt P\nextline
+246 & 166 & a6 & \verb*"\Sigma" & \mbox{$\Sigma$} & Alt S\nextline
+247 & 167 & a7 & \verb*"\Phi" & \mbox{$\Phi$} & Alt F\nextline
+250 & 168 & a8 & \verb*"\Psi" & \mbox{$\Psi$} & Alt Q\nextline
+251 & 169 & a9 & \verb*"\Omega" & \mbox{$\Omega$} & Alt W\nextline
+252 & 170 & aa & \verb*"'a" & \mbox{$\alpha$} & Alt a\nextline
+253 & 171 & ab & \verb*"'b" & \mbox{$\beta$} & Alt b\nextline
+254 & 172 & ac & \verb*"'c" & \mbox{$\gamma$} & Alt g\nextline
+255 & 173 & ad & \verb*"\delta" & \mbox{$\delta$} & Alt d\nextline
+256 & 174 & ae & \verb*"\varepsilon" & \mbox{$\varepsilon$} & Alt e\nextline
+257 & 175 & af & \verb*"\zeta" & \mbox{$\zeta$} & Alt z\nextline
+260 & 176 & b0 & \verb*"\eta" & \mbox{$\eta$} & Alt h\nextline
+261 & 177 & b1 & \verb*"\vartheta" & \mbox{$\vartheta$} & Alt j\nextline
+262 & 178 & b2 & \verb*"\kappa" & \mbox{$\kappa$} & Alt k\nextline
+263 & 179 & b3 & \verb*"%" & \mbox{$\lambda$} & Alt l\nextline
+264 & 180 & b4 & \verb*"\mu" & \mbox{$\mu$} & Alt m\nextline
+265 & 181 & b5 & \verb*"\nu" & \mbox{$\nu$} & Alt n\nextline
+266 & 182 & b6 & \verb*"\xi" & \mbox{$\xi$} & Alt x\nextline
+267 & 183 & b7 & \verb*"\pi" & \mbox{$\pi$} & Alt p\nextline
+270 & 184 & b8 & \verb*"'r" & \mbox{$\rho$} & Alt r\nextline
+271 & 185 & b9 & \verb*"'s" & \mbox{$\sigma$} & Alt s\nextline
+272 & 186 & ba & \verb*"'t" & \mbox{$\tau$} & Alt t\nextline
+273 & 187 & bb & \verb*"\varphi" & \mbox{$\varphi$} & Alt f\nextline
+274 & 188 & bc & \verb*"\chi" & \mbox{$\chi$} & Alt c\nextline
+275 & 189 & bd & \verb*"\psi" & \mbox{$\psi$} & Alt q\nextline
+276 & 190 & be & \verb*"\omega" & \mbox{$\omega$} & Alt w\nextline
+277 & 191 & bf & \verb*"~" & \mbox{$\neg$} & AltGraph n\nextline
+300 & 192 & c0 & \verb*"&" & \mbox{$\wedge$} & AltGraph a\nextline
+301 & 193 & c1 & \verb*"|" & \mbox{$\vee$} & AltGraph o\nextline
+302 & 194 & c2 & \verb*"!" & \mbox{$\forall$} & AltGraph f\nextline
+303 & 195 & c3 & \verb*"?" & \mbox{$\exists$} & AltGraph t\nextline
+304 & 196 & c4 & \verb*"!!" & \mbox{$\bigwedge$} & AltGraph F,  F9\nextline
+305 & 197 & c5 & \verb*"\lceil" & \mbox{$\lceil$} & Ctrl F5\nextline
+306 & 198 & c6 & \verb*"\rceil" & \mbox{$\rceil$} & Ctrl F6\nextline
+307 & 199 & c7 & \verb*"\lfloor" & \mbox{$\lfloor$} & Ctrl F7\nextline
+310 & 200 & c8 & \verb*"\rfloor" & \mbox{$\rfloor$} & Ctrl F8\nextline
+311 & 201 & c9 & \verb*"(|" & \mbox{$(\!|$} & Ctrl F9\nextline
+312 & 202 & ca & \verb*"|)" & \mbox{$|\!)$} & Ctrl F10\nextline
+313 & 203 & cb & \verb*"[|" & \mbox{$[\![$} & Ctrl F11\nextline
+314 & 204 & cc & \verb*"|]" & \mbox{$]\!]$} & Ctrl F12\nextline
+315 & 205 & cd & \verb*"\emptyset" & \mbox{$\emptyset$} & Alt F10\nextline
+316 & 206 & ce & \verb*":" & \mbox{$\in$} & Alt F11\nextline
+317 & 207 & cf & \verb*"\subseteq" & \mbox{$\subseteq$} & AltGraph F5\nextline
+320 & 208 & d0 & \verb*"Int" & \mbox{$\cap$} & AltGraph F1\nextline
+321 & 209 & d1 & \verb*"Un" & \mbox{$\cup$} & AltGraph F2\nextline
+322 & 210 & d2 & \verb*"Inter" & \mbox{$\bigcap$} & AltGraph F3\nextline
+323 & 211 & d3 & \verb*"Union" & \mbox{$\bigcup$} & AltGraph F4\nextline
+324 & 212 & d4 & \verb*"\sqcap" & \mbox{$\sqcap$} & Ctrl F1\nextline
+325 & 213 & d5 & \verb*"\sqcup" & \mbox{$\sqcup$} & Ctrl F2\nextline
+326 & 214 & d6 & \verb*"glb" & \mbox{$\overline{|\,\,|}$} & Ctrl F3\nextline
+327 & 215 & d7 & \verb*"lub" & \mbox{$\bigsqcup$} & Ctrl F4\nextline
+330 & 216 & d8 & \verb*"UU" & \mbox{$\perp$} & AltGraph b\nextline
+331 & 217 & d9 & \verb*"===" & \mbox{$\doteq$} & AltGraph e\nextline
+332 & 218 & da & \verb*"==" & \mbox{$\equiv$} & AltGraph E,  F11\nextline
+333 & 219 & db & \verb*"~=" & \mbox{$\not=$} & AltGraph u,  F12\nextline
+334 & 220 & dc & \verb*"\sqsubset" & \mbox{$\sqsubset$} & AltGraph p\nextline
+335 & 221 & dd & \verb*"<<" & \mbox{$\sqsubseteq$} & AltGraph P\nextline
+336 & 222 & de & \verb*"\prec" & \mbox{$\prec$} & AltGraph l\nextline
+337 & 223 & df & \verb*"\preceq" & \mbox{$\preceq$} & AltGraph L\nextline
+340 & 224 & e0 & \verb*"\succ" & \mbox{$\succ$} & AltGraph g\nextline
+341 & 225 & e1 & \verb*"\succeq" & \mbox{$\succeq$} & AltGraph G\nextline
+342 & 226 & e2 & \verb*"\sim" & \mbox{$\sim$} & AltGraph s\nextline
+343 & 227 & e3 & \verb*"\simeq" & \mbox{$\simeq$} & AltGraph S\nextline
+344 & 228 & e4 & \verb*"\le" & \mbox{$\le$} & Shift F11\nextline
+345 & 229 & e5 & \verb*"\ge" & \mbox{$\ge$} & Shift F12\nextline
+346 & 230 & e6 & \verb*"<-" & \mbox{$\leftarrow$} & Alt F1\nextline
+347 & 231 & e7 & \verb*"-" & \mbox{$-$} & Alt F2\nextline
+350 & 232 & e8 & \verb*"->" & \mbox{$\rightarrow$} & Alt F3, AltGraph m\nextline
+351 & 233 & e9 & \verb*"<=" & \mbox{$\Leftarrow$} & Shift F1\nextline
+352 & 234 & ea & \verb*"=" & \mbox{$=$} & Shift F2\nextline
+353 & 235 & eb & \verb*"=>" & \mbox{$\Rightarrow$} & Shift F3, AltGraph M\nextline
+354 & 236 & ec & \verb*"->>" & \mbox{$\twoheadrightarrow$} & Alt F5\nextline
+355 & 237 & ed & \verb*"\mapsto" & \mbox{$\mapsto$} & Alt F6\nextline
+356 & 238 & ee & \verb*"\leadsto" & \mbox{$\leadsto$} & Alt F7\nextline
+357 & 239 & ef & \verb*"\uparrow" & \mbox{$\uparrow$} & Alt F8\nextline
+360 & 240 & f0 & \verb*"\downarrow" & \mbox{$\downarrow$} & Alt F9\nextline
+361 & 241 & f1 & \verb*"~:" & \mbox{$\notin$} & Alt F12\nextline
+362 & 242 & f2 & \verb*"*" & \mbox{$\times$} & AltGraph x\nextline
+363 & 243 & f3 & \verb*"++" & \mbox{$\oplus$} & Shift F5\nextline
+364 & 244 & f4 & \verb*"\ominus" & \mbox{$\ominus$} & Shift F6\nextline
+365 & 245 & f5 & \verb*"**" & \mbox{$\otimes$} & Shift F7\nextline
+366 & 246 & f6 & \verb*"\oslash" & \mbox{$\oslash$} & Shift F8\nextline
+367 & 247 & f7 & \verb*"\natural" & \mbox{$\natural$} & Shift F9, AltGraph N\nextline
+370 & 248 & f8 & \verb*"\infty" & \mbox{$\infty$} & Shift F10\nextline
+371 & 249 & f9 & \verb*"\Box" & \mbox{$\Box$} & AltGraph F6\nextline
+372 & 250 & fa & \verb*"\Diamond" & \mbox{$\Diamond$} & AltGraph F7\nextline
+373 & 251 & fb & \verb*"\circ" & \mbox{$\circ$} & AltGraph F8\nextline
+374 & 252 & fc & \verb*"\bullet" & \mbox{$\bullet$} & AltGraph F9\nextline
+375 & 253 & fd & \verb*"||" & \mbox{$\parallel$} & AltGraph F10\nextline
+376 & 254 & fe & \verb*"\tick" & \mbox{$\surd$} & AltGraph F11\nextline
+377 & 255 & ff & \verb*"\filter" & \mbox{\copyright} & AltGraph F12\\
+\end{supertabular}
+\end{center}
+\end{document}
Binary file src/Tools/8bit/doc/keyindex.dvi has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/keyindex.tex	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,128 @@
+\documentclass[a4paper,11pt]{article}
+\usepackage{latexsym,amssymb,supertab}
+
+\begin{document}
+
+\begin{center}
+{\Large 
+  Description of Keyboard Mapping\\
+      Indexed by Key Sequence}\\
+  Date: \today 
+
+\vspace*{.5cm}
+
+\tablehead{\hline
+Key Sequence & Code Sequence in Hex & \LaTeX \\
+\hline}
+\tabletail{\hline}
+
+\begin{supertabular}{|l|l|l|}
+ F9 & c4 & \mbox{$\bigwedge$}\nextline
+ F10 & ea,eb & \mbox{$\Longrightarrow$}\nextline
+ F11 & da & \mbox{$\equiv$}\nextline
+ F12 & db & \mbox{$\not=$}\nextline
+Ctrl F1 & d4 & \mbox{$\sqcap$}\nextline
+Ctrl F2 & d5 & \mbox{$\sqcup$}\nextline
+Ctrl F3 & d6 & \mbox{$\overline{|\,\,|}$}\nextline
+Ctrl F4 & d7 & \mbox{$\bigsqcup$}\nextline
+Ctrl F5 & c5 & \mbox{$\lceil$}\nextline
+Ctrl F6 & c6 & \mbox{$\rceil$}\nextline
+Ctrl F7 & c7 & \mbox{$\lfloor$}\nextline
+Ctrl F8 & c8 & \mbox{$\rfloor$}\nextline
+Ctrl F9 & c9 & \mbox{$(\!|$}\nextline
+Ctrl F10 & ca & \mbox{$|\!)$}\nextline
+Ctrl F11 & cb & \mbox{$[\![$}\nextline
+Ctrl F12 & cc & \mbox{$]\!]$}\nextline
+Alt D & a2 & \mbox{$\Delta$}\nextline
+Alt F & a7 & \mbox{$\Phi$}\nextline
+Alt G & a1 & \mbox{$\Gamma$}\nextline
+Alt J & a3 & \mbox{$\Theta$}\nextline
+Alt L & a4 & \mbox{$\Lambda$}\nextline
+Alt P & a5 & \mbox{$\Pi$}\nextline
+Alt Q & a8 & \mbox{$\Psi$}\nextline
+Alt S & a6 & \mbox{$\Sigma$}\nextline
+Alt W & a9 & \mbox{$\Omega$}\nextline
+Alt a & aa & \mbox{$\alpha$}\nextline
+Alt b & ab & \mbox{$\beta$}\nextline
+Alt c & bc & \mbox{$\chi$}\nextline
+Alt d & ad & \mbox{$\delta$}\nextline
+Alt e & ae & \mbox{$\varepsilon$}\nextline
+Alt f & bb & \mbox{$\varphi$}\nextline
+Alt g & ac & \mbox{$\gamma$}\nextline
+Alt h & b0 & \mbox{$\eta$}\nextline
+Alt j & b1 & \mbox{$\vartheta$}\nextline
+Alt k & b2 & \mbox{$\kappa$}\nextline
+Alt l & b3 & \mbox{$\lambda$}\nextline
+Alt m & b4 & \mbox{$\mu$}\nextline
+Alt n & b5 & \mbox{$\nu$}\nextline
+Alt p & b7 & \mbox{$\pi$}\nextline
+Alt q & bd & \mbox{$\psi$}\nextline
+Alt r & b8 & \mbox{$\rho$}\nextline
+Alt s & b9 & \mbox{$\sigma$}\nextline
+Alt t & ba & \mbox{$\tau$}\nextline
+Alt w & be & \mbox{$\omega$}\nextline
+Alt x & b6 & \mbox{$\xi$}\nextline
+Alt z & af & \mbox{$\zeta$}\nextline
+Alt F1 & e6 & \mbox{$\leftarrow$}\nextline
+Alt F2 & e7 & \mbox{$-$}\nextline
+Alt F3 & e8 & \mbox{$\rightarrow$}\nextline
+Alt F4 & e6,e8 & \mbox{$\leftrightarrow$}\nextline
+Alt F5 & ec & \mbox{$\twoheadrightarrow$}\nextline
+Alt F6 & ed & \mbox{$\mapsto$}\nextline
+Alt F7 & ee & \mbox{$\leadsto$}\nextline
+Alt F8 & ef & \mbox{$\uparrow$}\nextline
+Alt F9 & f0 & \mbox{$\downarrow$}\nextline
+Alt F10 & cd & \mbox{$\emptyset$}\nextline
+Alt F11 & ce & \mbox{$\in$}\nextline
+Alt F12 & f1 & \mbox{$\notin$}\nextline
+AltGraph E & da & \mbox{$\equiv$}\nextline
+AltGraph F & c4 & \mbox{$\bigwedge$}\nextline
+AltGraph G & e1 & \mbox{$\succeq$}\nextline
+AltGraph I & ea,eb & \mbox{$\Longrightarrow$}\nextline
+AltGraph L & df & \mbox{$\preceq$}\nextline
+AltGraph M & eb & \mbox{$\Rightarrow$}\nextline
+AltGraph N & f7 & \mbox{$\natural$}\nextline
+AltGraph P & dd & \mbox{$\sqsubseteq$}\nextline
+AltGraph S & e3 & \mbox{$\simeq$}\nextline
+AltGraph a & c0 & \mbox{$\wedge$}\nextline
+AltGraph b & d8 & \mbox{$\perp$}\nextline
+AltGraph e & d9 & \mbox{$\doteq$}\nextline
+AltGraph f & c2 & \mbox{$\forall$}\nextline
+AltGraph g & e0 & \mbox{$\succ$}\nextline
+AltGraph i & e7,e8 & \mbox{$\longrightarrow$}\nextline
+AltGraph l & de & \mbox{$\prec$}\nextline
+AltGraph m & e8 & \mbox{$\rightarrow$}\nextline
+AltGraph n & bf & \mbox{$\neg$}\nextline
+AltGraph o & c1 & \mbox{$\vee$}\nextline
+AltGraph p & dc & \mbox{$\sqsubset$}\nextline
+AltGraph s & e2 & \mbox{$\sim$}\nextline
+AltGraph t & c3 & \mbox{$\exists$}\nextline
+AltGraph u & db & \mbox{$\not=$}\nextline
+AltGraph x & f2 & \mbox{$\times$}\nextline
+AltGraph F1 & d0 & \mbox{$\cap$}\nextline
+AltGraph F2 & d1 & \mbox{$\cup$}\nextline
+AltGraph F3 & d2 & \mbox{$\bigcap$}\nextline
+AltGraph F4 & d3 & \mbox{$\bigcup$}\nextline
+AltGraph F5 & cf & \mbox{$\subseteq$}\nextline
+AltGraph F6 & f9 & \mbox{$\Box$}\nextline
+AltGraph F7 & fa & \mbox{$\Diamond$}\nextline
+AltGraph F8 & fb & \mbox{$\circ$}\nextline
+AltGraph F9 & fc & \mbox{$\bullet$}\nextline
+AltGraph F10 & fd & \mbox{$\parallel$}\nextline
+AltGraph F11 & fe & \mbox{$\surd$}\nextline
+AltGraph F12 & ff & \mbox{\copyright}\nextline
+Shift F1 & e9 & \mbox{$\Leftarrow$}\nextline
+Shift F2 & ea & \mbox{$=$}\nextline
+Shift F3 & eb & \mbox{$\Rightarrow$}\nextline
+Shift F4 & e9,eb & \mbox{$\Leftrightarrow$}\nextline
+Shift F5 & f3 & \mbox{$\oplus$}\nextline
+Shift F6 & f4 & \mbox{$\ominus$}\nextline
+Shift F7 & f5 & \mbox{$\otimes$}\nextline
+Shift F8 & f6 & \mbox{$\oslash$}\nextline
+Shift F9 & f7 & \mbox{$\natural$}\nextline
+Shift F10 & f8 & \mbox{$\infty$}\nextline
+Shift F11 & e4 & \mbox{$\le$}\nextline
+Shift F12 & e5 & \mbox{$\ge$}\\
+\end{supertabular}
+\end{center}
+\end{document}
Binary file src/Tools/8bit/doc/manual.dvi has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/manual.itex	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,388 @@
+\documentclass[]{article}
+\usepackage{latexsym,amssymb,isa2latex}
+
+\newcommand{\bt}[1]{{\tt #1}}
+
+\title{The Isabelle 8bit Package}
+\author{
+David von Oheimb and Franz Regensburger\\
+Technical University of Munich, Germany\\
+E-mail: \bt{\{oheimb|regensbu\}@informatik.tu-muenchen.de}
+}
+\date{\today}
+
+\begin{document}
+\maketitle
+
+
+
+
+\section{Introduction}
+
+The 8bit package enables you to view, edit and print Isabelle files and perform
+proofs in a quite pleasant form. 
+
+Instead of representing logical operators with ASCII character sequences, 
+a special graphical character font, resp. 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
+ASCII 7bit character coding with (non-standard) character codes having the
+8th bit set. All this is described in section \ref{graph} of this manual.
+
+Even without employing the 8bit font, the \LaTeX{} output for 
+Isabelle files can be used for manuals, papers etc. This is the focus of
+section \ref{latex}.
+
+
+
+
+\section{Graphical Isabelle}
+\label{graph}
+
+This section describes the main purpose of the 8bit package, which is to provide
+an extension to the ASCII character set that allows to formulate and display 
+many logical operators as graphical symbols. 
+
+\subsection{Usage}
+
+To employ the graphical font within Isabelle, just (re-)formulate the 
+logical operators of your Isabelle theory (and proof) files using this font. 
+A graphical terminal and suitable editors are described in subsection 
+\ref{commands}.
+
+As a typical example, consider the following fragment of an Isabelle theory, 
+an alternative formulation of the bounded universal quantifier within the 
+set theory of \bt{HOL}.
+
+\label{ex}
+Without graphical characters, the operator is defined as follows.
+\I@isa
+consts	
+    	Ball	:: "'a set => ('a => bool) => bool"
+syntax
+	"@Ball"	:: "pttrn => 'a set => bool => bool"	("(3!_:_./ _)" 10)
+translations
+		"!x:A. P" == "Ball A (%x. P)"
+defs
+     Ball_def	"Ball A P == ! x. x:A --> P x"
+\I@isa
+
+Using the graphical font (and assuming a corresponding re-formulation of 
+\bt{HOL} operators), the definition of the operator can be improved to the following.
+
+\I@isa
+consts
+	Ball	:: "'a set  ('a  bool)  bool"
+syntax
+	"GBall"	:: "pttrn  'a set  bool  bool"	("(3__./ _)" 10)
+translations
+		"xA. P" == "Ball A (x. P)"
+defs
+     Ball_def	"Ball A P  x. xA  P x"
+\I@isa
+
+Note the appearance of the graphical characters, which makes the code much more
+legible.
+
+\label{compat}
+It is also possible to retain pure ASCII versions of the logical operators while
+offering the possibility of graphical input and output.
+This may be necessary for compatibility reasons or for providing
+graphical versions of the meta logic \I@Pure\I@ or object logics already
+defined. In these cases, the graphical syntax can be supplied additionally with 
+appropriate \I@types\I@, \I@syntax\I@, and \I@translations\I@ sections, as done
+for example in the Isabelle distribution of \bt{HOL}.
+
+In the example given above, the ASCII formulation of the quantifier can be
+augmented with a graphical version by the following definition.
+
+\I@isa
+syntax
+	"GBall"	:: "pttrn => 'a set => bool => bool"	("(3__./ _)" 10)
+translations
+		"xA. P" == "!x:A. P"
+\I@isa
+
+With this approach, the operators can still be entered in ASCII form, which is
+important for the usability of old (pure ASCII) Isabelle files, while they are
+displayed in the new graphical form. The additional level of syntax 
+translations introduced in this way may interfere with other translation rules
+and should therefore be designed carefully.
+
+
+\subsection{User commands}
+\label{commands}
+
+
+A number of commands for manipulating files with graphical characters are 
+available, as described in this subsection.
+
+\subsubsection{Editors}
+
+The first group of commands includes versions of the most common editors that 
+can handle the graphical font for both keyboard input and display input. 
+See the files \bt{doc/\{fontindex|keyindex|fkmatrix\}.dvi} for the keystrokes
+defined for inputting the special characters. The editors are
+
+\begin{itemize}
+\item \bt{isa\_xemacs}		replaces \bt{xemacs}. You may provide a 
+				specific init file called 
+				\bt{.emacs\_isa\_xemacs} (in your home directory)
+				that is executed after the \bt{.emacs} file.
+\item \bt{isa\_gnu\_emacs}	replaces \bt{emacs}. You may provide a 
+				specific init file called 
+				\bt{.emacs\_isa\_gnu\_emacs} (in your home 
+				directory) that is executed after the 
+				\bt{.emacs} file.
+\item \bt{isaaxe}		replaces \bt{axe}
+\item \bt{isavim}		replaces \bt{vim}
+\end{itemize}
+
+For example, as \bt{emacs} user you may type
+\bt{isa\_xemacs doc/Set2g.thy \&} to view and edit
+the above sample theory fragment.
+
+\subsubsection{Display commands}
+
+The next group of commands is used to display files using the graphical font.
+With the terminal, of course also input is possible, using the same keystrokes
+as with the editors.
+
+\begin{itemize}
+\item \bt{isaterm} 		replaces \bt{xterm}. This is used as terminal
+				for your ML interpreter running Isabelle with
+				theories and proofs containing graphical 
+				characters. This terminal is also useful if
+				you want to \bt{cat} or \bt{grep} the Isabelle
+				files within your shell, and as
+				environment for commands like \bt{isapal}.
+\item \bt{isapal}		shows the palette of available graphical 
+				characters. A man page is available.
+\item \bt{codetable}		prints all 8bit characters with their codes
+\item \bt{isa\_xmosaic}	replaces \bt{xmosaic}. This is useful for
+				browsing the index files of Isabelle theories
+				(with graphical operators) that are generated
+				if \I@make_html\I@ is set to \I@true\I@.
+\end{itemize}
+
+\subsubsection{Converters}
+\label{conv}
+
+The last group of commands is built to enable conversion between ASCII, 8bit 
+font and
+\LaTeX\ representations of the graphical characters within papers, manuals, 
+and Isabelle theory and proof files. For the options of the converters, see 
+the corresponding man pages.
+
+\begin{itemize}
+\item \bt{isa2latex}	converts a file with 8bit characters to a LaTeX
+			source. Pure ASCII input and conversion of 8bit 
+			characters to their ASCII representations is also 
+			possible.
+\item \bt{a2isa}	converts Isabelle files, from ASCII to 8bit characters.
+			It is used mainly to convert old files.
+\end{itemize}
+
+In order to output the first theory fragment (formulated without the 8bit
+font) in subsection \ref{ex} as LaTeX\ source using suitable graphical 
+characters, type\\
+\bt{isa2latex -s -A -o Set2.tex doc/Set2\_a.thy}.\\
+(It was necessary to insert some blank characters in the file \bt{Set2\_a.thy} 
+that enable \bt{isa2latex} to recognize all the operators intended to be 
+printed with graphical characters, as discussed in subsection \ref{ambig}.)
+
+For conversion of \bt{Set2.thy} to 8bit characters, type\\
+\bt{a2isa -o Set2\_g.thy doc/Set2.thy}.
+
+Further explanations of the use of the converter \bt{isa2latex} are given
+in section \ref{latex}.
+
+
+
+
+\section{\LaTeX\ output}
+\label{latex}
+
+Independently of whether Isabelle files are formulated with the graphical font
+or not, they can be converted to \LaTeX\ source using \bt{isa2latex}
+and in this way (pretty-)printed with the familiar symbols for quantification, 
+intersection, etc. The tool \bt{isa2latex} can also convert \LaTeX\ source
+files containing Isabelle source to pure \LaTeX\ 
+files, by converting the special character sequences of the Isabelle parts to
+appropriate \LaTeX\ commands, and handing through the rest (almost) verbatim.
+
+For example, this manual itself is converted to a \bt{.tex} file by \\
+\bt{isa2latex -x -e -o manual.tex doc/manual.itex}
+
+\subsection{Conversion modes}
+
+To handle the different parts of an input file, \bt{isa2latex} has several 
+conversion modes, namely
+\begin{itemize}
+\item \bt{LATEX}: The input is is literally copied to the output,
+without conversion of any characters. This mode is used for the \LaTeX\ parts
+ of the input document.
+
+\item \bt{INLINE}: The conversion of characters and scanning for 
+multi character sequences is active, while newline and tab characters are 
+treated as single blank character.
+Use this mode for inserting small parts of Isabelle source within 
+a line of text.
+
+\item \bt{ISA}: The conversion of characters and scanning for 
+multi character sequences is active, while newline and tab characters are 
+treated according to an open tabbing environment. 
+This mode is used for displaying multiple lines of Isabelle source.
+
+\item \bt{ESC}: In this mode the input is literally copied to the output.
+This mode is intended as an escape mode from the \bt{INLINE} and \bt{ESC} modes.
+\end{itemize}
+
+Upon entrance of the conversion modes, \bt{isa2latex} generates the \LaTeX\ 
+commands \bt{\mbox{$\backslash$}isamode} for \bt{ISA}, 
+\bt{\mbox{$\backslash$}isainline} for \bt{INLINE}, 
+and \bt{\mbox{$\backslash$}isaescape} for the \bt{ESC} mode. These act as
+environment delimiters and may also set the appropriate fonts, styles etc. The 
+commands 
+are defined in the file \bt{latex/isa2latex.sty} and may be adapted as desired.
+
+\subsection{Conversion mode switching}
+
+The initial conversion mode of \bt{isa2latex} and the set of available modes 
+depend on the options given on the command line. Switching of the modes
+relies on special toggles (like \I@\I\E@\E@@isa\I@, within the input
+file) that indicate the beginning and end of the different parts of the input.
+
+The following diagrams show the initial mode (enclosed in sqare brackets), 
+the available mode switches (in the arrow symbols)
+and the modes reachable with them.
+
+If the \bt{-x} option is not given:
+
+\I@isa
+[ISA]  <-- \E\E@\E@@ -->  ESC
+\I@isa
+
+If the \bt{-x} option is given:
+
+\I@isa
+[LATEX]  <-- \I\E@\E@@ -->  INLINE  <-- \E\E@\E@@ -->  ESC
+   ^
+   |------ \I\E@\E@@isa -->  ISA  <-- \E\E@\E@@ -->  ESC
+\I@isa
+
+
+\subsection{Ambiguity problems}
+\label{ambig}
+
+As \bt{isa2latex} converts its input files on a lexical level, it has limited
+capability of dealing with ambiguities that are caused by using the same 
+characters for different operators. A typical examle
+is the `\I@|\I@' character, which is used within the object logic \bt{HOL} both
+as disjunction operator and as separator within \I@case\I@ expressions. In the
+former case, it should be converted to `\I@\I@', and in the latter case 
+retained as `\I@|\I@'. 
+
+As a workaround, in the current version of \bt{isa2latex},
+such ``dangerous'' characters are converted only if followed by a blank 
+character. Thus to enforce a conversion, append a blank character behind it, and
+to prohibit it even if a blank character follows, you may insert a double 
+\I@\E\E@\E@@\I@, i.e. the string becomes `\I@|\E\E@\E@@\E\E@\E@@ \I@'. 
+
+You may also redefine the critical entries of the conversion tables in the file
+\bt{config/conv-tables.inp}. The entry for the `\I@|\I@' character
+looks like
+\I@isa
+>  "\|\ "		"|"		"\mbox{$\vee$}" 
+\I@isa
+The first string, which (as described by the verbose comments in that file)
+is the lex expression for the ASCII input, could be adapted to require an 
+additional blank character before the `\I@|\I@', for example.
+
+Most of these amibiguity problems can be avoided if you decide to employ the
+graphical font for your Isabelle source files. In this case, we recommend 
+using this font as early as possible, in order to avoid later conversions.
+For the conversion of old files, the tool \bt{a2isa} is provided. It
+normally requires no changes of the original files and only minor corrections
+of the files it produces. Thus the preferred way is to apply \bt{a2isa} once and
+for all on the source files, correct all conversion mistakes, and then use the 
+new files with the graphical font. With these files, the ambiguity problems 
+should have gone.
+
+As the converter \bt{a2isa} is a bit smarter than \bt{isa2latex} in converting
+ASCII input, it is also useful if you do not employ the 8bit font directly. To
+convert a problematic ASCII file containing Isabelle source, first apply
+\bt{a2isa} and then \bt{isa2latex} without option \bt{-A}. For example, type\\
+\bt{a2isa Set2.thy | isa2latex -s -o doc/Set2a.tex}\\
+to generate a better output than in the example conversion given in subsection
+\ref{conv}.
+
+
+\section{Technical issues}
+
+\subsection{Preparations}
+
+To use the 8bit package, you have to set resp. extend the content of the 
+following environment variables:
+
+\begin{itemize}
+\item \bt{ISABELLE8BIT}: set the directory of the Isabelle 8bit package,\\
+	e.g.  \bt{/usr/proj/isabelle/src/Tools/8bit}
+
+\item \bt{PATH}: add the absolute path of the executables,\\
+	e.g.  \bt{\$ISABELLE8BIT/bin}
+
+\item \bt{MANPATH}: add the absolute path of the manual pages,\\
+	e.g.  \bt{\$ISABELLE8BIT/man}
+
+\item \bt{TEXINPUTS}: add the absolute path of special LaTeX style files
+			used by the 8bit package (if necessary),
+	e.g. \bt{\$ISABELLE8BIT/latex:}\\
+                the trailing `\bt{:}' makes latex search subdirectories!\\
+	The 8bit package uses
+	\begin{itemize}
+	\item the AMSFONT package
+        \item the supertab style (clarkson)	
+        \item the special style \bt{isa2latex.sty}
+	\end{itemize}
+	Some of them are contained in that directory.
+\end{itemize}
+
+Before the first use of any executable of subdirectory {\tt bin}, call
+the scripts \bt{fonts/install} and \bt{keyboard/install}. This is done best
+in your \bt{.login} file.
+
+\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.
+
+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},
+and run \bt{gmake} in this directory to generate new versions of 
+\bt{isa2latex}, editor support, and documentation.
+
+For adapting the conversion table of \bt{a2isa}, change directory to \\
+\bt{\$ISABELLE8BIT/c-sources/a2isa}, edit the file \bt{lex.x}
+accordingly, and run \bt{gmake} there.
+
+\subsection{Management of alternative sources}
+
+If you retain ASCII versions of logical operators for compatibility reasons,
+as described in subsection \ref{compat}, you may want to export versions of your
+Isabelle theories that contain no 8bit characters. To support this, a patching
+mechanism is provided as follows. Encapsulate each section of your files dealing
+solely with the 8bit font with suitable begin and end pragmas (some pair of 
+unique comment lines) and configure three configuration files analogously to\\
+\bt{\$ISABELLE8BIT/isa-patches/HOL/\{extract|clean|add\}-HOL.cfg}.
+Then you can call the \bt{patcher} with the first file to extract and store to
+a file, the second to remove, and the third to re-add the 8bit section of the
+Isabelle files. See also the man page of \bt{patcher}.
+
+
+\end{document}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/palette.isa	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,19 @@
+      
+
+      
+
+          
+
+               
+
+          
+           
+
+      
+        
+      
+
+            
+         
+
+         
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/bash.inputrc	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,3 @@
+set meta-flag On
+set convert-meta Off
+set output-meta On
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/bdf-code.txt	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,29 @@
+BBX line
+
+BBX 5 13 2 -2
+
+means character
+	extends 5 pixels to the right
+	is 13 Pixels high
+	left margin is 2 pixels 
+	descend from base line is 2 pixels	
+
+
+hex-bin code table for the hacker
+
+0	0	0000
+1	1	0001
+2	2	0010
+3	3	0011
+4	4	0100
+5	5	0101
+6	6	0110
+7	7	0111
+8	8	1000
+9	9	1001
+10	a	1010
+11	b	1011
+12	c	1100
+13	d	1101
+14	e	1110
+15	f	1111
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/fonts.dir	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,5 @@
+4
+spcr14.bdf spcr14
+isacr14.bdf isacr14
+isacb24.bdf isacb24
+oldisacr14.bdf oldisacr14
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/install	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,8 @@
+#!/bin/bash
+# add Isabelle 8bit fonts to X11 font path
+
+FONTDIR=$ISABELLE8BIT/fonts
+
+# remove it first to avoid accidental double inclusion
+xset fp- $FONTDIR 2>/dev/null
+xset fp+ $FONTDIR
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/isacb24.bdf	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,3936 @@
+STARTFONT 2.1
+FONT spcb24
+SIZE 24 75 75
+FONTBOUNDINGBOX 16 22 6 -5
+STARTPROPERTIES 22
+FONTNAME_REGISTRY ""
+FAMILY_NAME "Courier"
+FOUNDRY "Adobe"
+WEIGHT_NAME "Bold"
+SLANT "R"
+SETWIDTH_NAME "Normal"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 24
+POINT_SIZE 240
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "M"
+AVERAGE_WIDTH 150
+CHARSET_REGISTRY "ISO8859"
+CHARSET_ENCODING "1"
+CHARSET_COLLECTIONS "ASCII ISO8859-1 ADOBE-STANDARD"
+FULL_NAME "Courier Bold"
+COPYRIGHT "Copyright (c)1985,1987 Adobe Systems, Inc., Portions Copyright 1988"
+FONT_ASCENT 17
+FONT_DESCENT 5
+CAP_HEIGHT 15
+X_HEIGHT 11
+ENDPROPERTIES
+CHARS 205
+STARTCHAR space
+ENCODING 32
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR exclam
+ENCODING 33
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 4 16 5 0
+BITMAP
+60
+f0
+f0
+f0
+f0
+f0
+f0
+f0
+60
+60
+60
+60
+00
+00
+60
+60
+ENDCHAR
+STARTCHAR quotedbl
+ENCODING 34
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 7 3 8
+BITMAP
+e7
+e7
+e7
+e7
+c6
+84
+84
+ENDCHAR
+STARTCHAR numbersign
+ENCODING 35
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 19 1 -2
+BITMAP
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+7ff0
+7ff0
+1980
+1980
+1980
+ffe0
+ffe0
+3300
+3300
+3300
+3300
+3300
+3300
+ENDCHAR
+STARTCHAR dollar
+ENCODING 36
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 20 2 -3
+BITMAP
+0c00
+0c00
+3d80
+7f80
+c380
+c180
+c000
+e000
+7e00
+1f80
+01c0
+00c0
+c0c0
+e1c0
+ff80
+df00
+0c00
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR percent
+ENCODING 37
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 2 0
+BITMAP
+3c00
+6600
+4200
+4200
+6600
+3c00
+01c0
+0f00
+3800
+e780
+0cc0
+0840
+0840
+0cc0
+0780
+ENDCHAR
+STARTCHAR ampersand
+ENCODING 38
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 14 2 0
+BITMAP
+1e00
+3f00
+6300
+6000
+6000
+3000
+3800
+7cc0
+6fc0
+c780
+c300
+c780
+ffe0
+7ce0
+ENDCHAR
+STARTCHAR quoteright
+ENCODING 39
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 6 4 9
+BITMAP
+38
+38
+70
+60
+c0
+80
+ENDCHAR
+STARTCHAR parenleft
+ENCODING 40
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 6 -4
+BITMAP
+18
+38
+30
+60
+60
+60
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+60
+60
+60
+30
+38
+18
+ENDCHAR
+STARTCHAR parenright
+ENCODING 41
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 3 -4
+BITMAP
+c0
+e0
+60
+30
+30
+30
+18
+18
+18
+18
+18
+18
+18
+18
+30
+30
+30
+60
+e0
+c0
+ENDCHAR
+STARTCHAR asterisk
+ENCODING 42
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 11 2 5
+BITMAP
+0c00
+0c00
+0c00
+ccc0
+edc0
+3f00
+0c00
+1e00
+3300
+7380
+6180
+ENDCHAR
+STARTCHAR plus
+ENCODING 43
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0600
+0600
+0600
+0600
+0600
+0600
+fff0
+fff0
+0600
+0600
+0600
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR comma
+ENCODING 44
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 6 4 -3
+BITMAP
+38
+38
+70
+60
+c0
+80
+ENDCHAR
+STARTCHAR minus
+ENCODING 45
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 2 1 6
+BITMAP
+fff0
+fff0
+ENDCHAR
+STARTCHAR period
+ENCODING 46
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 3 3 5 0
+BITMAP
+e0
+e0
+e0
+ENDCHAR
+STARTCHAR slash
+ENCODING 47
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 20 2 -3
+BITMAP
+0060
+0060
+00c0
+00c0
+0180
+0180
+0300
+0300
+0600
+0600
+0c00
+0c00
+1800
+1800
+3000
+3000
+6000
+6000
+c000
+c000
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1e00
+7f80
+6180
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+6180
+7f80
+1e00
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1c00
+fc00
+fc00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 0
+BITMAP
+1f80
+3fc0
+70e0
+6060
+6060
+0060
+00e0
+01c0
+0380
+0700
+0e00
+1c00
+3800
+7000
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR three
+ENCODING 51
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 0
+BITMAP
+1f80
+3fc0
+70e0
+6060
+0060
+00e0
+01c0
+0f80
+0fc0
+00e0
+0060
+0060
+c060
+e0e0
+7fc0
+3f80
+ENDCHAR
+STARTCHAR four
+ENCODING 52
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 0
+BITMAP
+0380
+0780
+0f80
+0d80
+1980
+1980
+3180
+3180
+6180
+6180
+ffe0
+ffe0
+0180
+0180
+0fe0
+0fe0
+ENDCHAR
+STARTCHAR five
+ENCODING 53
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 2 0
+BITMAP
+7fc0
+7fc0
+6000
+6000
+6000
+6f00
+7fc0
+71c0
+00e0
+0060
+0060
+0060
+c0e0
+e1c0
+7fc0
+3f00
+ENDCHAR
+STARTCHAR six
+ENCODING 54
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 3 0
+BITMAP
+07c0
+1fc0
+3c00
+7000
+6000
+e000
+cf00
+df80
+f1c0
+e0c0
+c0c0
+c0c0
+e0c0
+71c0
+7f80
+1f00
+ENDCHAR
+STARTCHAR seven
+ENCODING 55
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+ffc0
+ffc0
+c0c0
+00c0
+0180
+0180
+0180
+0300
+0300
+0300
+0600
+0600
+0600
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR eight
+ENCODING 56
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1e00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+6180
+3f00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+3f00
+ENDCHAR
+STARTCHAR nine
+ENCODING 57
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 3 0
+BITMAP
+1e00
+7f80
+6180
+c0c0
+c0c0
+c0c0
+c0c0
+c1c0
+e3c0
+7ec0
+3cc0
+00c0
+0180
+0380
+ff00
+fc00
+ENDCHAR
+STARTCHAR colon
+ENCODING 58
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 3 11 5 0
+BITMAP
+e0
+e0
+e0
+00
+00
+00
+00
+00
+e0
+e0
+e0
+ENDCHAR
+STARTCHAR semicolon
+ENCODING 59
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 14 3 -3
+BITMAP
+38
+38
+38
+00
+00
+00
+00
+00
+38
+38
+70
+60
+c0
+80
+ENDCHAR
+STARTCHAR less
+ENCODING 60
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 12 1 1
+BITMAP
+0038
+00f0
+03c0
+0f00
+3c00
+f000
+f000
+3c00
+0f00
+03c0
+00f0
+0038
+ENDCHAR
+STARTCHAR equal
+ENCODING 61
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 6 1 4
+BITMAP
+fff0
+fff0
+0000
+0000
+fff0
+fff0
+ENDCHAR
+STARTCHAR greater
+ENCODING 62
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 12 1 1
+BITMAP
+e000
+7800
+1e00
+0780
+01e0
+0078
+0078
+01e0
+0780
+1e00
+7800
+e000
+ENDCHAR
+STARTCHAR question
+ENCODING 63
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 15 3 0
+BITMAP
+7e00
+ff00
+c380
+c180
+c180
+0180
+0380
+0f00
+1c00
+1800
+1800
+0000
+0000
+1800
+1800
+ENDCHAR
+STARTCHAR at
+ENCODING 64
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 18 2 -2
+BITMAP
+1c00
+7f00
+6300
+c180
+c180
+c780
+cf80
+dd80
+d980
+d980
+dd80
+cfc0
+c7c0
+c000
+c000
+6180
+7f80
+1e00
+ENDCHAR
+STARTCHAR A
+ENCODING 65
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+3f00
+3f80
+0780
+0780
+0cc0
+0cc0
+1ce0
+1860
+1860
+3ff0
+3ff0
+7038
+6018
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR B
+ENCODING 66
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+ffc0
+ffe0
+3070
+3030
+3030
+3070
+3fe0
+3ff0
+3038
+3018
+3018
+3018
+3038
+fff0
+ffe0
+ENDCHAR
+STARTCHAR C
+ENCODING 67
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+0fd8
+3ff8
+7038
+6018
+e018
+c000
+c000
+c000
+c000
+c000
+e000
+6018
+7038
+3ff0
+0fc0
+ENDCHAR
+STARTCHAR D
+ENCODING 68
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+ffc0
+fff0
+3038
+3018
+301c
+300c
+300c
+300c
+300c
+300c
+300c
+3018
+3038
+fff0
+ffe0
+ENDCHAR
+STARTCHAR E
+ENCODING 69
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+fff0
+fff0
+3030
+3030
+3030
+3180
+3180
+3f80
+3f80
+3180
+3198
+3018
+3018
+fff8
+fff8
+ENDCHAR
+STARTCHAR F
+ENCODING 70
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+fff8
+fff8
+3018
+3018
+3018
+3180
+3180
+3f80
+3f80
+3180
+3180
+3000
+3000
+ff00
+ff00
+ENDCHAR
+STARTCHAR G
+ENCODING 71
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+0fd8
+3ff8
+7038
+6018
+e018
+c000
+c000
+c000
+c1f8
+c1f8
+e018
+6018
+7038
+3ff0
+0fc0
+ENDCHAR
+STARTCHAR H
+ENCODING 72
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcfc
+fcfc
+3030
+3030
+3030
+3030
+3ff0
+3ff0
+3030
+3030
+3030
+3030
+3030
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR I
+ENCODING 73
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 2 0
+BITMAP
+ffc0
+ffc0
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR J
+ENCODING 74
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+1ff8
+1ff8
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+3f00
+ENDCHAR
+STARTCHAR K
+ENCODING 75
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcf8
+fcf8
+30e0
+31c0
+3380
+3700
+3e00
+3f00
+3b80
+31c0
+30e0
+3060
+3070
+fc3c
+fc3c
+ENDCHAR
+STARTCHAR L
+ENCODING 76
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+ff00
+ff00
+1800
+1800
+1800
+1800
+1800
+1800
+1800
+1800
+1830
+1830
+1830
+fff0
+fff0
+ENDCHAR
+STARTCHAR M
+ENCODING 77
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+f03c
+f03c
+7878
+7878
+7878
+6cd8
+6cd8
+6798
+6798
+6318
+6018
+6018
+6018
+f87c
+f87c
+ENDCHAR
+STARTCHAR N
+ENCODING 78
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+f0f8
+f0f8
+7830
+7830
+6c30
+6c30
+6630
+6630
+6330
+6330
+61b0
+61b0
+60f0
+f8f0
+f870
+ENDCHAR
+STARTCHAR O
+ENCODING 79
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+0f80
+3fe0
+7070
+6030
+e038
+c018
+c018
+c018
+c018
+c018
+e038
+6030
+7070
+3fe0
+0f80
+ENDCHAR
+STARTCHAR P
+ENCODING 80
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+ffc0
+fff0
+3038
+3018
+3018
+3018
+3018
+3038
+3ff0
+3fc0
+3000
+3000
+3000
+ff00
+ff00
+ENDCHAR
+STARTCHAR Q
+ENCODING 81
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 18 1 -3
+BITMAP
+0f80
+3fe0
+7070
+6030
+e038
+c018
+c018
+c018
+c018
+c018
+e038
+6030
+7070
+3fe0
+0f80
+1e18
+3ff8
+39e0
+ENDCHAR
+STARTCHAR R
+ENCODING 82
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+ff80
+ffe0
+3070
+3030
+3030
+3030
+3070
+3fe0
+3f80
+31c0
+30e0
+3060
+3070
+fc3c
+fc3c
+ENDCHAR
+STARTCHAR S
+ENCODING 83
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+1fb0
+3ff0
+7070
+6030
+6030
+7000
+3e00
+1fc0
+03e0
+0070
+c030
+c030
+e070
+ffe0
+dfc0
+ENDCHAR
+STARTCHAR T
+ENCODING 84
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+fff0
+fff0
+c630
+c630
+c630
+c630
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+3fc0
+3fc0
+ENDCHAR
+STARTCHAR U
+ENCODING 85
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+f8f8
+f8f8
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+3060
+3fe0
+1fc0
+ENDCHAR
+STARTCHAR V
+ENCODING 86
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+f87c
+f87c
+6018
+6018
+3030
+3030
+3030
+1860
+1860
+1860
+0cc0
+0cc0
+0780
+0780
+0780
+ENDCHAR
+STARTCHAR W
+ENCODING 87
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+f87c
+f87c
+6018
+6318
+6318
+6798
+6798
+6fd8
+6cd8
+6cd8
+3cf0
+3870
+3870
+3870
+3870
+ENDCHAR
+STARTCHAR X
+ENCODING 88
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcfc
+fcfc
+7038
+3870
+1ce0
+0fc0
+0780
+0300
+0780
+0cc0
+1ce0
+3870
+7038
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR Y
+ENCODING 89
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcfc
+fcfc
+7038
+3870
+1860
+0cc0
+0fc0
+0780
+0300
+0300
+0300
+0300
+0300
+1fe0
+1fe0
+ENDCHAR
+STARTCHAR Z
+ENCODING 90
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 15 2 0
+BITMAP
+ffe0
+ffe0
+c0e0
+c1c0
+c380
+0300
+0700
+0e00
+1c00
+1800
+3860
+7060
+e060
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR bracketleft
+ENCODING 91
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 6 -4
+BITMAP
+f8
+f8
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+f8
+f8
+ENDCHAR
+STARTCHAR backslash
+ENCODING 92
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 20 2 -3
+BITMAP
+c000
+c000
+6000
+6000
+3000
+3000
+1800
+1800
+0c00
+0c00
+0600
+0600
+0300
+0300
+0180
+0180
+00c0
+00c0
+0060
+0060
+ENDCHAR
+STARTCHAR bracketright
+ENCODING 93
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 3 -4
+BITMAP
+f8
+f8
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+f8
+f8
+ENDCHAR
+STARTCHAR asciicircum
+ENCODING 94
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 8 3 8
+BITMAP
+18
+18
+3c
+3c
+66
+66
+c3
+c3
+ENDCHAR
+STARTCHAR underscore
+ENCODING 95
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 15 2 0 -4
+BITMAP
+fffe
+fffe
+ENDCHAR
+STARTCHAR quoteleft
+ENCODING 96
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 6 5 9
+BITMAP
+e0
+e0
+70
+30
+18
+08
+ENDCHAR
+STARTCHAR a
+ENCODING 97
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+3f00
+7f80
+61c0
+00c0
+1fc0
+7fc0
+e0c0
+c0c0
+c1c0
+fff0
+7ef0
+ENDCHAR
+STARTCHAR b
+ENCODING 98
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 0 0
+BITMAP
+f000
+f000
+3000
+3000
+3000
+37c0
+3ff0
+3c70
+3838
+3018
+3018
+3018
+3838
+3c70
+fff0
+f7c0
+ENDCHAR
+STARTCHAR c
+ENCODING 99
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 11 1 0
+BITMAP
+1fb0
+7ff0
+70f0
+e070
+c030
+c000
+c000
+e000
+7038
+7ff8
+1fe0
+ENDCHAR
+STARTCHAR d
+ENCODING 100
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 0
+BITMAP
+01e0
+01e0
+0060
+0060
+0060
+1f60
+7fe0
+71e0
+e0e0
+c060
+c060
+c060
+e0e0
+71e0
+7ff8
+1f78
+ENDCHAR
+STARTCHAR e
+ENCODING 101
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+1f80
+7fe0
+70e0
+e070
+c030
+fff0
+fff0
+e000
+7070
+7ff0
+1fc0
+ENDCHAR
+STARTCHAR f
+ENCODING 102
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 2 0
+BITMAP
+07e0
+0fe0
+1c00
+1800
+1800
+ffc0
+ffc0
+1800
+1800
+1800
+1800
+1800
+1800
+1800
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR g
+ENCODING 103
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 -5
+BITMAP
+1f78
+7ff8
+71e0
+e0e0
+c060
+c060
+c060
+e0e0
+71e0
+7fe0
+1f60
+0060
+0060
+00e0
+3fc0
+3f80
+ENDCHAR
+STARTCHAR h
+ENCODING 104
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 16 0 0
+BITMAP
+f000
+f000
+3000
+3000
+3000
+37c0
+3fe0
+3c70
+3830
+3030
+3030
+3030
+3030
+3030
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR i
+ENCODING 105
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1c00
+1c00
+1c00
+0000
+0000
+7c00
+7c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR j
+ENCODING 106
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 21 2 -5
+BITMAP
+0e
+0e
+0e
+00
+00
+ff
+ff
+03
+03
+03
+03
+03
+03
+03
+03
+03
+03
+03
+07
+fe
+fc
+ENDCHAR
+STARTCHAR k
+ENCODING 107
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 0
+BITMAP
+f000
+f000
+3000
+3000
+3000
+31e0
+31e0
+3380
+3700
+3e00
+3e00
+3700
+3380
+31c0
+f1f8
+f1f8
+ENDCHAR
+STARTCHAR l
+ENCODING 108
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+7c00
+7c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR m
+ENCODING 109
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 16 11 0 0
+BITMAP
+ef78
+fffc
+39cc
+318c
+318c
+318c
+318c
+318c
+318c
+f9ef
+f9ef
+ENDCHAR
+STARTCHAR n
+ENCODING 110
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+f3c0
+f7e0
+3c70
+3830
+3030
+3030
+3030
+3030
+3030
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR o
+ENCODING 111
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+1f80
+7fe0
+70e0
+e070
+c030
+c030
+c030
+e070
+70e0
+7fe0
+1f80
+ENDCHAR
+STARTCHAR p
+ENCODING 112
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 0 -5
+BITMAP
+f7c0
+fff0
+3c70
+3838
+3018
+3018
+3018
+3838
+3c70
+3ff0
+37c0
+3000
+3000
+3000
+fe00
+fe00
+ENDCHAR
+STARTCHAR q
+ENCODING 113
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 -5
+BITMAP
+1f78
+7ff8
+71e0
+e0e0
+c060
+c060
+c060
+e0e0
+71e0
+7fe0
+1f60
+0060
+0060
+0060
+03f8
+03f8
+ENDCHAR
+STARTCHAR r
+ENCODING 114
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+79e0
+7ff0
+1e30
+1c00
+1800
+1800
+1800
+1800
+1800
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR s
+ENCODING 115
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 2 0
+BITMAP
+3ec0
+7fc0
+e1c0
+e0c0
+7c00
+1f00
+07c0
+c0e0
+e0e0
+ffc0
+df80
+ENDCHAR
+STARTCHAR t
+ENCODING 116
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 15 1 0
+BITMAP
+3000
+3000
+3000
+3000
+ffc0
+ffc0
+3000
+3000
+3000
+3000
+3000
+3000
+38e0
+1fe0
+0f80
+ENDCHAR
+STARTCHAR u
+ENCODING 117
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+f0f0
+f0f0
+3030
+3030
+3030
+3030
+3030
+3030
+3870
+1ffc
+0fbc
+ENDCHAR
+STARTCHAR v
+ENCODING 118
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+fcfc
+fcfc
+3030
+3030
+1860
+1860
+0cc0
+0cc0
+0780
+0780
+0300
+ENDCHAR
+STARTCHAR w
+ENCODING 119
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+f87c
+f87c
+6318
+6318
+3330
+37b0
+37b0
+3cf0
+1ce0
+1860
+1860
+ENDCHAR
+STARTCHAR x
+ENCODING 120
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+f9f0
+f9f0
+30c0
+1980
+0f00
+0600
+0f00
+1980
+30c0
+f9f0
+f9f0
+ENDCHAR
+STARTCHAR y
+ENCODING 121
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 16 0 -5
+BITMAP
+f87c
+f87c
+3030
+3870
+1860
+1ce0
+0cc0
+0dc0
+0780
+0780
+0300
+0700
+0600
+0e00
+7f00
+7f00
+ENDCHAR
+STARTCHAR z
+ENCODING 122
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 11 2 0
+BITMAP
+ffc0
+ffc0
+c380
+c700
+0e00
+1c00
+3800
+70c0
+e0c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR braceleft
+ENCODING 123
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 20 4 -4
+BITMAP
+0e
+18
+30
+30
+30
+30
+30
+30
+70
+e0
+70
+30
+30
+30
+30
+30
+30
+30
+18
+0e
+ENDCHAR
+STARTCHAR bar
+ENCODING 124
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 2 18 6 -2
+BITMAP
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+ENDCHAR
+STARTCHAR braceright
+ENCODING 125
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 20 3 -4
+BITMAP
+e0
+30
+18
+18
+18
+18
+18
+18
+1c
+0e
+1c
+18
+18
+18
+18
+18
+18
+18
+30
+e0
+ENDCHAR
+STARTCHAR asciitilde
+ENCODING 126
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 4 1 5
+BITMAP
+3c30
+7e70
+e7e0
+c3c0
+ENDCHAR
+STARTCHAR space
+ENCODING 128
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 129
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 130
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 131
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 132
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 133
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 134
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 135
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 136
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 137
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 138
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 139
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 140
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 141
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 160
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR Gamma
+ENCODING 161
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+60c0
+60c0
+60c0
+6000
+6000
+6000
+6000
+6000
+6000
+6000
+f000
+f000
+ENDCHAR
+STARTCHAR Delta
+ENCODING 162
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 12 1 0
+BITMAP
+0200
+0700
+0700
+0d80
+0d80
+18c0
+18c0
+3060
+3060
+6030
+fff8
+fff8
+ENDCHAR
+STARTCHAR Theta
+ENCODING 163
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 14 1 0
+BITMAP
+3e00
+7f00
+6300
+c180
+c180
+c180
+ff80
+ff80
+c180
+c180
+c180
+6300
+7f00
+3e00
+ENDCHAR
+STARTCHAR Lambda
+ENCODING 164
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 13 1 0
+BITMAP
+0400
+0400
+0e00
+0e00
+1b00
+1b00
+1100
+3180
+3180
+2080
+60c0
+60c0
+f1e0
+ENDCHAR
+STARTCHAR C167
+ENCODING 165
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 14 1 0
+BITMAP
+fff8
+fff8
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+ENDCHAR
+STARTCHAR C167
+ENCODING 166
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 14 1 0
+BITMAP
+fff8
+fff8
+6018
+3000
+1800
+0c00
+0600
+0600
+0c00
+1800
+3000
+6018
+fff8
+fff8
+ENDCHAR
+STARTCHAR C167
+ENCODING 167
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0f00
+0600
+0600
+1f80
+6660
+4620
+8610
+8610
+8610
+4620
+6660
+1f80
+0600
+0f00
+ENDCHAR
+STARTCHAR C167
+ENCODING 168
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0f00
+0600
+0600
+c630
+6660
+6660
+6660
+6660
+6660
+36c0
+1f80
+0f00
+0600
+0f00
+ENDCHAR
+STARTCHAR C167
+ENCODING 169
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0f00
+3fc0
+70e0
+6060
+c030
+c030
+c030
+c030
+6060
+6060
+30c0
+1980
+f9f0
+f9f0
+ENDCHAR
+STARTCHAR a
+ENCODING 170
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 10 1 0
+BITMAP
+1f18
+3f98
+71b0
+61f0
+e0e0
+c0c0
+c0e0
+c1f0
+7fb8
+3e18
+ENDCHAR
+STARTCHAR C177
+ENCODING 171
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 -3
+BITMAP
+0780
+0fc0
+0ce0
+1860
+1860
+30c0
+33c0
+33c0
+30e0
+6060
+6060
+60e0
+67c0
+c700
+c000
+c000
+ENDCHAR
+STARTCHAR C177
+ENCODING 172
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 13 1 -3
+BITMAP
+6000
+f0c0
+9bc0
+0f00
+0e00
+1c00
+1e00
+3600
+3600
+6600
+6600
+3c00
+1800
+ENDCHAR
+STARTCHAR C170
+ENCODING 173
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 2 0
+BITMAP
+1e00
+3100
+3000
+3000
+1c00
+0f00
+3f80
+71c0
+60c0
+c0c0
+c180
+e380
+7f00
+3c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 174
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 12 1 0
+BITMAP
+1c
+3e
+72
+60
+38
+38
+60
+c0
+c0
+e6
+7e
+3c
+ENDCHAR
+STARTCHAR C177
+ENCODING 175
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 16 1 -3
+BITMAP
+08
+0c
+1f
+30
+60
+60
+c0
+c0
+c0
+c0
+c0
+60
+3c
+0e
+06
+06
+ENDCHAR
+STARTCHAR C177
+ENCODING 176
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 -4
+BITMAP
+6600
+ef00
+b980
+3180
+3180
+6300
+6300
+6300
+0600
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR C177
+ENCODING 177
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+0780
+0cc0
+0cc0
+0cc0
+0780
+6180
+b300
+3300
+3300
+6600
+6600
+3c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 178
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 8 1 0
+BITMAP
+c780
+6c00
+3800
+3800
+3c00
+3400
+6680
+c300
+ENDCHAR
+STARTCHAR C177
+ENCODING 179
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 13 1 0
+BITMAP
+6000
+3000
+1800
+1800
+0c00
+0c00
+1c00
+1600
+3600
+2600
+6300
+4300
+c180
+ENDCHAR
+STARTCHAR C177
+ENCODING 180
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 -4
+BITMAP
+3180
+3180
+3180
+3180
+6300
+6300
+7f80
+7f80
+c000
+c000
+c000
+c000
+ENDCHAR
+STARTCHAR C177
+ENCODING 181
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 8 1 0
+BITMAP
+63
+b3
+33
+33
+66
+66
+7c
+78
+ENDCHAR
+STARTCHAR C167
+ENCODING 182
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 15 1 -2
+BITMAP
+1e
+30
+60
+60
+60
+3e
+30
+60
+c0
+c0
+c0
+7c
+06
+06
+0c
+ENDCHAR
+STARTCHAR C177
+ENCODING 183
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 9 1 0
+BITMAP
+3c20
+ffe0
+9bc0
+1980
+1980
+3180
+3180
+3180
+3180
+ENDCHAR
+STARTCHAR C177
+ENCODING 184
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 12 1 -4
+BITMAP
+0c
+1e
+33
+63
+63
+66
+3c
+38
+30
+30
+60
+c0
+ENDCHAR
+STARTCHAR C167
+ENCODING 185
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 7 1 0
+BITMAP
+1f80
+3e00
+6600
+c600
+c600
+cc00
+7800
+ENDCHAR
+STARTCHAR C167
+ENCODING 186
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 9 1 0
+BITMAP
+7f80
+ff00
+9800
+1800
+1800
+3000
+3000
+3200
+1c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 187
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 -4
+BITMAP
+0700
+4f80
+9cc0
+98c0
+98c0
+d8c0
+7f80
+1f00
+0c00
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 188
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 -4
+BITMAP
+60c0
+3180
+3180
+1b00
+1b00
+1e00
+0c00
+1c00
+3c00
+6600
+6600
+c300
+ENDCHAR
+STARTCHAR C167
+ENCODING 189
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 13 1 -3
+BITMAP
+0600
+0600
+2640
+e660
+6660
+6660
+6660
+66c0
+36c0
+1f00
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR C167
+ENCODING 190
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 7 1 0
+BITMAP
+6060
+c630
+c630
+c630
+c630
+6660
+1f80
+ENDCHAR
+STARTCHAR C160
+ENCODING 191
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 9 7 2 0
+BITMAP
+ff80
+ff80
+0380
+0380
+0380
+0380
+0380
+ENDCHAR
+STARTCHAR C161
+ENCODING 192
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 9 2 0
+BITMAP
+0c00
+1e00
+1e00
+3300
+3300
+6180
+6180
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 193
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 9 2 0
+BITMAP
+c0c0
+c0c0
+6180
+6180
+3300
+3300
+1e00
+1e00
+0c00
+ENDCHAR
+STARTCHAR C166
+ENCODING 194
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+8040
+c0c0
+c0c0
+4080
+7f80
+7f80
+2100
+3300
+3300
+1200
+1e00
+1e00
+0c00
+0c00
+ENDCHAR
+STARTCHAR C167
+ENCODING 195
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+01c0
+01c0
+01c0
+01c0
+ffc0
+ffc0
+01c0
+01c0
+01c0
+01c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C166
+ENCODING 196
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 -1
+BITMAP
+0600
+0600
+0f00
+0f00
+0900
+1980
+1980
+1080
+30c0
+30c0
+2040
+6060
+6060
+4020
+c030
+ENDCHAR
+STARTCHAR C197
+ENCODING 197
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+ffc0
+ffc0
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+ENDCHAR
+STARTCHAR C197
+ENCODING 198
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+ffc0
+ffc0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+ENDCHAR
+STARTCHAR C197
+ENCODING 199
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C197
+ENCODING 200
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C201
+ENCODING 201
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 15 1 -1
+BITMAP
+06
+0e
+1e
+36
+66
+c6
+c6
+c6
+c6
+c6
+66
+36
+1e
+0e
+06
+ENDCHAR
+STARTCHAR C201
+ENCODING 202
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 15 1 -1
+BITMAP
+c0
+e0
+f0
+d8
+cc
+c6
+c6
+c6
+c6
+c6
+cc
+d8
+f0
+e0
+c0
+ENDCHAR
+STARTCHAR C203
+ENCODING 203
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C204
+ENCODING 204
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR o
+ENCODING 205
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 1 0
+BITMAP
+1f60
+7fe0
+71c0
+e3e0
+c760
+ce60
+dc60
+f8e0
+71c0
+ffc0
+df00
+ENDCHAR
+STARTCHAR C177
+ENCODING 206
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 0
+BITMAP
+1f80
+3f80
+6000
+6000
+c000
+ff00
+ff00
+c000
+6000
+6000
+3f80
+1f80
+ENDCHAR
+STARTCHAR C161
+ENCODING 207
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 1 0
+BITMAP
+1fe0
+7fe0
+e000
+c000
+c000
+e000
+7fe0
+1fe0
+0000
+7fe0
+7fe0
+ENDCHAR
+STARTCHAR C161
+ENCODING 208
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+1e00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 209
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+1e00
+ENDCHAR
+STARTCHAR C197
+ENCODING 210
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+1e00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C197
+ENCODING 211
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+1e00
+ENDCHAR
+STARTCHAR C161
+ENCODING 212
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+ffc0
+ffc0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 213
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C197
+ENCODING 214
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+ffc0
+ffc0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C197
+ENCODING 215
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C161
+ENCODING 216
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 10 1 0
+BITMAP
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+fff0
+fff0
+ENDCHAR
+STARTCHAR C161
+ENCODING 217
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 9 1 4
+BITMAP
+0600
+0600
+0000
+fff0
+fff0
+0000
+0000
+fff0
+fff0
+ENDCHAR
+STARTCHAR C177
+ENCODING 218
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 8 1 1
+BITMAP
+ff80
+ff80
+0000
+ff80
+ff80
+0000
+ff80
+ff80
+ENDCHAR
+STARTCHAR C161
+ENCODING 219
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 2
+BITMAP
+0300
+0700
+ffc0
+ffc0
+0e00
+1c00
+ffc0
+ffc0
+3800
+3000
+ENDCHAR
+STARTCHAR C161
+ENCODING 220
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 8 1 3
+BITMAP
+ffe0
+ffe0
+c000
+c000
+c000
+c000
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR C161
+ENCODING 221
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 1 1
+BITMAP
+ffe0
+ffe0
+c000
+c000
+c000
+c000
+ffe0
+ffe0
+0000
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR C177
+ENCODING 222
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+0040
+00c0
+0180
+0300
+0e00
+f800
+f800
+0e00
+0300
+0180
+00c0
+0040
+ENDCHAR
+STARTCHAR C177
+ENCODING 223
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 -2
+BITMAP
+0040
+00c0
+0180
+0300
+0e00
+f800
+f800
+0e00
+0300
+0180
+00c0
+0000
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C177
+ENCODING 224
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+8000
+c000
+6000
+3000
+1c00
+07c0
+07c0
+1c00
+3000
+6000
+c000
+8000
+ENDCHAR
+STARTCHAR C177
+ENCODING 225
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 -2
+BITMAP
+8000
+c000
+6000
+3000
+1c00
+07c0
+07c0
+1c00
+3000
+6000
+c000
+0000
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C161
+ENCODING 226
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 4 1 5
+BITMAP
+3800
+fe30
+c7f0
+01c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 227
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 7 1 4
+BITMAP
+3800
+fe30
+c7f0
+01c0
+0000
+fff0
+fff0
+ENDCHAR
+STARTCHAR C177
+ENCODING 228
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 0
+BITMAP
+0180
+0700
+1c00
+7000
+c000
+7000
+1c00
+0700
+0180
+0000
+ff80
+ff80
+ENDCHAR
+STARTCHAR C177
+ENCODING 229
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 0
+BITMAP
+c000
+7000
+1c00
+0700
+0180
+0700
+1c00
+7000
+c000
+0000
+ff80
+ff80
+ENDCHAR
+STARTCHAR leftarrow
+ENCODING 230
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 10 4 2
+BITMAP
+0c00
+1c00
+3800
+7000
+fff8
+fff8
+7000
+3800
+1c00
+0c00
+ENDCHAR
+STARTCHAR  hline
+ENCODING 231
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 16 2 1 6
+BITMAP
+ffff
+ffff
+ENDCHAR
+STARTCHAR rightarrow
+ENCODING 232
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 10 1 2
+BITMAP
+0180
+01c0
+00e0
+0070
+fff8
+fff8
+0070
+00e0
+01c0
+0180
+ENDCHAR
+STARTCHAR Leftarrow
+ENCODING 233
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 14 4 0
+BITMAP
+0300
+0700
+0e00
+1c00
+3ff8
+7ff8
+e000
+e000
+7ff8
+3ff8
+1c00
+0e00
+0700
+0300
+ENDCHAR
+STARTCHAR doublehline
+ENCODING 234
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 16 6 1 4
+BITMAP
+ffff
+ffff
+0000
+0000
+ffff
+ffff
+ENDCHAR
+STARTCHAR Rightarrow
+ENCODING 235
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 14 1 0
+BITMAP
+0600
+0700
+0380
+01c0
+ffe0
+fff0
+0038
+0038
+fff0
+ffe0
+01c0
+0380
+0700
+0600
+ENDCHAR
+STARTCHAR C161
+ENCODING 236
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 8 1 3
+BITMAP
+06c0
+0360
+01b0
+fff8
+fff8
+01b0
+0360
+06c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 237
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 10 1 2
+BITMAP
+0180
+c1c0
+c0e0
+c070
+fff8
+fff8
+c070
+c0e0
+c1c0
+0180
+ENDCHAR
+STARTCHAR C161
+ENCODING 238
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 10 1 2
+BITMAP
+00c0
+00e0
+0070
+3c38
+7efc
+e7fc
+c3b8
+0070
+00e0
+00c0
+ENDCHAR
+STARTCHAR C167
+ENCODING 239
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 13 1 0
+BITMAP
+0c00
+1e00
+3f00
+7f80
+edc0
+ccc0
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR C167
+ENCODING 240
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 13 1 0
+BITMAP
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ccc0
+edc0
+7f80
+3f00
+1e00
+0c00
+ENDCHAR
+STARTCHAR C161
+ENCODING 241
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 14 1 -1
+BITMAP
+0180
+1f80
+3f80
+6300
+6600
+c600
+ff00
+ff00
+d800
+7800
+7000
+3f80
+7f80
+6000
+ENDCHAR
+STARTCHAR C175
+ENCODING 242
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+c030
+6060
+30c0
+1980
+0f00
+0600
+0f00
+1980
+30c0
+6060
+c030
+ENDCHAR
+STARTCHAR plus
+ENCODING 243
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6318
+4308
+c30c
+dfec
+dfec
+c30c
+4308
+6318
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR plus
+ENCODING 244
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6018
+4008
+c00c
+dfec
+dfec
+c00c
+4008
+6018
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR plus
+ENCODING 245
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+7878
+5ce8
+cfcc
+c78c
+c78c
+cfcc
+5ce8
+7878
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR plus
+ENCODING 246
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6078
+40e8
+c1cc
+c38c
+c70c
+ce0c
+5c08
+7818
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR C247
+ENCODING 247
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 14 1 0
+BITMAP
+c0
+c0
+c6
+ce
+de
+f6
+e6
+ce
+de
+f6
+e6
+c6
+06
+06
+ENDCHAR
+STARTCHAR C161
+ENCODING 248
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 8 0 2
+BITMAP
+3870
+7cf8
+efdc
+c78c
+c78c
+efdc
+7cf8
+3870
+ENDCHAR
+STARTCHAR C161
+ENCODING 249
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 9 1 2
+BITMAP
+ff80
+ff80
+c180
+c180
+c180
+c180
+c180
+ff80
+ff80
+ENDCHAR
+STARTCHAR C161
+ENCODING 250
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 1
+BITMAP
+0c00
+1e00
+3f00
+7380
+e1c0
+e1c0
+7380
+3f00
+1e00
+0c00
+ENDCHAR
+STARTCHAR C161
+ENCODING 251
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 1
+BITMAP
+1e00
+7f80
+6180
+c0c0
+c0c0
+c0c0
+c0c0
+6180
+7f80
+1e00
+ENDCHAR
+STARTCHAR C161
+ENCODING 252
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 1
+BITMAP
+1e00
+7f80
+7f80
+ffc0
+ffc0
+ffc0
+ffc0
+7f80
+7f80
+1e00
+ENDCHAR
+STARTCHAR C253
+ENCODING 253
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 6 15 4 -1
+BITMAP
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+ENDCHAR
+STARTCHAR C254
+ENCODING 254
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 1
+BITMAP
+0070
+0070
+00c0
+00c0
+0180
+e180
+f300
+3300
+1e00
+1e00
+0c00
+ENDCHAR
+STARTCHAR plus
+ENCODING 255
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6798
+4cc8
+d80c
+d00c
+d00c
+d80c
+4cc8
+6798
+3030
+1fe0
+0780
+ENDCHAR
+ENDFONT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/isacr14.bdf	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,2977 @@
+STARTFONT 2.1
+COMMENT
+COMMENT  Copyright 1984, 1987 Adobe Systems, Inc.
+COMMENT  Portions Copyright 1988 Digital Equipment Corporation
+COMMENT  Portions Copyright 1993 TU Muenchen, Germany
+COMMENT
+COMMENT  Adobe is a registered trademark of Adobe Systems, Inc.  Permission
+COMMENT  to use these trademarks is hereby granted only in association with the
+COMMENT  images described in this file.
+COMMENT
+COMMENT  Permission to use, copy, modify, and distribute this software and
+COMMENT  its documentation for any purpose and without fee is hereby granted,
+COMMENT  provided that the above copyright notices appear in all copies and
+COMMENT  that both those copyright notices and this permission notice appear
+COMMENT  in supporting documentation, and that the names of Adobe Systems,
+COMMENT  Digital Equipment Corporation, and TU Muenchen not be used in
+COMMENT  advertising or publicity pertaining to distribution of the software
+COMMENT  without specific, written prior permission.  Adobe Systems, Digital
+COMMENT  Equipment Corporation, and TU Muenchen  make no representations about
+COMMENT  the suitability of this software for any purpose.  It is provided "as
+COMMENT  is" without express or implied warranty.
+COMMENT
+COMMENT  ADOBE SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN DISCLAIM
+COMMENT  ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL IMPLIED
+COMMENT  WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO EVENT SHALL ADOBE
+COMMENT  SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN BE LIABLE FOR 
+COMMENT  ANY SPECIAL, INDIRECT OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+COMMENT  WHATSOEVE RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+COMMENT  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT 
+COMMENT  OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+FONT isacr14
+SIZE 14 75 75
+FONTBOUNDINGBOX 9 14 4 -3
+STARTPROPERTIES 22
+FONTNAME_REGISTRY ""
+FAMILY_NAME "Isabelle"
+FOUNDRY ""
+WEIGHT_NAME "Medium"
+SLANT "R"
+SETWIDTH_NAME "Normal"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 14
+POINT_SIZE 140
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "M"
+AVERAGE_WIDTH 90
+CHARSET_REGISTRY ""
+CHARSET_ENCODING "1"
+CHARSET_COLLECTIONS ""
+FULL_NAME "Isabelle14"
+COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1993 TU Muenchen"
+FONT_ASCENT 11
+FONT_DESCENT 3
+CAP_HEIGHT 9
+X_HEIGHT 7
+ENDPROPERTIES
+CHARS 191
+STARTCHAR space
+ENCODING 32
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR exclam
+ENCODING 33
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 10 3 0
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+00
+00
+80
+ENDCHAR
+STARTCHAR quotedbl
+ENCODING 34
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 4 2 5
+BITMAP
+90
+90
+90
+90
+ENDCHAR
+STARTCHAR numbersign
+ENCODING 35
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+50
+50
+50
+f8
+50
+f8
+50
+50
+50
+ENDCHAR
+STARTCHAR dollar
+ENCODING 36
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 13 2 -2
+BITMAP
+20
+20
+78
+88
+80
+c0
+30
+08
+88
+f0
+20
+20
+20
+ENDCHAR
+STARTCHAR percent
+ENCODING 37
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+60
+90
+90
+66
+18
+30
+cc
+12
+12
+0c
+ENDCHAR
+STARTCHAR ampersand
+ENCODING 38
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+38
+48
+40
+40
+a8
+90
+98
+64
+ENDCHAR
+STARTCHAR quoteright
+ENCODING 39
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 5
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR parenleft
+ENCODING 40
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+20
+40
+40
+80
+80
+80
+80
+80
+80
+40
+40
+20
+ENDCHAR
+STARTCHAR parenright
+ENCODING 41
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+80
+40
+40
+20
+20
+20
+20
+20
+20
+40
+40
+80
+ENDCHAR
+STARTCHAR asterisk
+ENCODING 42
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 6 1 3
+BITMAP
+20
+20
+f8
+20
+50
+88
+ENDCHAR
+STARTCHAR plus
+ENCODING 43
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+fe
+10
+10
+10
+ENDCHAR
+STARTCHAR comma
+ENCODING 44
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 -2
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR minus
+ENCODING 45
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 1 1 4
+BITMAP
+fe
+ENDCHAR
+STARTCHAR period
+ENCODING 46
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 2 2 3 0
+BITMAP
+c0
+c0
+ENDCHAR
+STARTCHAR slash
+ENCODING 47
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+04
+08
+08
+10
+10
+20
+20
+40
+40
+80
+80
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+84
+84
+84
+84
+84
+84
+78
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 10 1 0
+BITMAP
+20
+60
+a0
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+04
+08
+10
+20
+40
+84
+fc
+ENDCHAR
+STARTCHAR three
+ENCODING 51
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+04
+04
+38
+04
+04
+04
+84
+78
+ENDCHAR
+STARTCHAR four
+ENCODING 52
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+18
+28
+28
+48
+48
+88
+88
+fc
+08
+1c
+ENDCHAR
+STARTCHAR five
+ENCODING 53
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+7c
+40
+40
+40
+78
+04
+04
+04
+84
+78
+ENDCHAR
+STARTCHAR six
+ENCODING 54
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+38
+40
+80
+80
+b8
+c4
+84
+84
+44
+38
+ENDCHAR
+STARTCHAR seven
+ENCODING 55
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+fc
+84
+04
+08
+08
+08
+10
+10
+10
+10
+ENDCHAR
+STARTCHAR eight
+ENCODING 56
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+84
+78
+84
+84
+84
+84
+78
+ENDCHAR
+STARTCHAR nine
+ENCODING 57
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+70
+88
+84
+84
+8c
+74
+04
+04
+08
+70
+ENDCHAR
+STARTCHAR colon
+ENCODING 58
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 2 7 3 0
+BITMAP
+c0
+c0
+00
+00
+00
+c0
+c0
+ENDCHAR
+STARTCHAR semicolon
+ENCODING 59
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 9 2 -2
+BITMAP
+60
+60
+00
+00
+00
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR less
+ENCODING 60
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+06
+18
+60
+80
+60
+18
+06
+ENDCHAR
+STARTCHAR equal
+ENCODING 61
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 3 1 3
+BITMAP
+fe
+00
+fe
+ENDCHAR
+STARTCHAR greater
+ENCODING 62
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+c0
+30
+0c
+02
+0c
+30
+c0
+ENDCHAR
+STARTCHAR question
+ENCODING 63
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 1 0
+BITMAP
+70
+88
+88
+08
+10
+20
+20
+00
+20
+ENDCHAR
+STARTCHAR at
+ENCODING 64
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+38
+44
+84
+9c
+a4
+a4
+9e
+80
+40
+38
+ENDCHAR
+STARTCHAR A
+ENCODING 65
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+3800
+0800
+1400
+1400
+2200
+3e00
+4100
+4100
+f780
+ENDCHAR
+STARTCHAR B
+ENCODING 66
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fc
+42
+42
+42
+7c
+42
+42
+42
+fc
+ENDCHAR
+STARTCHAR C
+ENCODING 67
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+3a
+46
+82
+80
+80
+80
+80
+42
+3c
+ENDCHAR
+STARTCHAR D
+ENCODING 68
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+fc
+42
+41
+41
+41
+41
+41
+42
+fc
+ENDCHAR
+STARTCHAR E
+ENCODING 69
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+42
+42
+48
+78
+48
+42
+42
+fe
+ENDCHAR
+STARTCHAR F
+ENCODING 70
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+42
+42
+48
+78
+48
+40
+40
+f0
+ENDCHAR
+STARTCHAR G
+ENCODING 71
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+3a
+46
+82
+80
+80
+8f
+82
+42
+3c
+ENDCHAR
+STARTCHAR H
+ENCODING 72
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+42
+42
+42
+7e
+42
+42
+42
+e7
+ENDCHAR
+STARTCHAR I
+ENCODING 73
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+f8
+20
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR J
+ENCODING 74
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+3e
+08
+08
+08
+08
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR K
+ENCODING 75
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+ee
+44
+48
+50
+70
+48
+44
+44
+e3
+ENDCHAR
+STARTCHAR L
+ENCODING 76
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+f8
+20
+20
+20
+20
+21
+21
+21
+ff
+ENDCHAR
+STARTCHAR M
+ENCODING 77
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+e380
+6300
+5700
+5500
+4900
+4900
+4100
+4100
+e380
+ENDCHAR
+STARTCHAR N
+ENCODING 78
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+62
+52
+52
+4a
+4a
+46
+46
+e2
+ENDCHAR
+STARTCHAR O
+ENCODING 79
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+3c
+42
+81
+81
+81
+81
+81
+42
+3c
+ENDCHAR
+STARTCHAR P
+ENCODING 80
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fc
+42
+42
+42
+42
+7c
+40
+40
+f0
+ENDCHAR
+STARTCHAR Q
+ENCODING 81
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 11 0 -2
+BITMAP
+3c
+42
+81
+81
+81
+81
+81
+42
+3c
+31
+5e
+ENDCHAR
+STARTCHAR R
+ENCODING 82
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+fc
+42
+42
+42
+44
+78
+44
+42
+e1
+ENDCHAR
+STARTCHAR S
+ENCODING 83
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 9 1 0
+BITMAP
+74
+8c
+84
+80
+78
+04
+84
+c4
+b8
+ENDCHAR
+STARTCHAR T
+ENCODING 84
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+92
+92
+10
+10
+10
+10
+10
+7c
+ENDCHAR
+STARTCHAR U
+ENCODING 85
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+42
+42
+42
+42
+42
+42
+42
+3c
+ENDCHAR
+STARTCHAR V
+ENCODING 86
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+e380
+4100
+4100
+2200
+2200
+1400
+1400
+0800
+0800
+ENDCHAR
+STARTCHAR W
+ENCODING 87
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+e380
+4100
+4900
+4900
+5500
+5500
+2200
+2200
+2200
+ENDCHAR
+STARTCHAR X
+ENCODING 88
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+42
+24
+24
+18
+24
+24
+42
+e7
+ENDCHAR
+STARTCHAR Y
+ENCODING 89
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+ee
+44
+44
+28
+28
+10
+10
+10
+7c
+ENDCHAR
+STARTCHAR Z
+ENCODING 90
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 9 1 0
+BITMAP
+fc
+84
+88
+10
+20
+20
+44
+84
+fc
+ENDCHAR
+STARTCHAR bracketleft
+ENCODING 91
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+e0
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+e0
+ENDCHAR
+STARTCHAR backslash
+ENCODING 92
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+80
+40
+40
+20
+20
+10
+10
+08
+08
+04
+04
+ENDCHAR
+STARTCHAR bracketright
+ENCODING 93
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+e0
+20
+20
+20
+20
+20
+20
+20
+20
+20
+20
+e0
+ENDCHAR
+STARTCHAR asciicircum
+ENCODING 94
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 5 2 4
+BITMAP
+20
+50
+50
+88
+88
+ENDCHAR
+STARTCHAR underscore
+ENCODING 95
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 1 0 -3
+BITMAP
+ff80
+ENDCHAR
+STARTCHAR quoteleft
+ENCODING 96
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 5
+BITMAP
+c0
+c0
+60
+20
+ENDCHAR
+STARTCHAR a
+ENCODING 97
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+78
+84
+04
+7c
+84
+8c
+76
+ENDCHAR
+STARTCHAR b
+ENCODING 98
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+c0
+40
+40
+5c
+62
+41
+41
+41
+62
+dc
+ENDCHAR
+STARTCHAR c
+ENCODING 99
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+3a
+46
+82
+80
+80
+42
+3c
+ENDCHAR
+STARTCHAR d
+ENCODING 100
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+06
+02
+02
+3a
+46
+82
+82
+82
+46
+3b
+ENDCHAR
+STARTCHAR e
+ENCODING 101
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+38
+44
+82
+fe
+80
+42
+3c
+ENDCHAR
+STARTCHAR f
+ENCODING 102
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+1e
+20
+20
+fc
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR g
+ENCODING 103
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+3b
+46
+82
+82
+82
+46
+3a
+02
+04
+78
+ENDCHAR
+STARTCHAR h
+ENCODING 104
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+c0
+40
+40
+5c
+62
+42
+42
+42
+42
+e7
+ENDCHAR
+STARTCHAR i
+ENCODING 105
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 10 2 0
+BITMAP
+20
+20
+00
+e0
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR j
+ENCODING 106
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 13 1 -3
+BITMAP
+10
+10
+00
+f8
+08
+08
+08
+08
+08
+08
+08
+10
+e0
+ENDCHAR
+STARTCHAR k
+ENCODING 107
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+c0
+40
+4e
+48
+50
+60
+50
+48
+ce
+ENDCHAR
+STARTCHAR l
+ENCODING 108
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+e0
+20
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR m
+ENCODING 109
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 7 0 0
+BITMAP
+db00
+6d00
+4900
+4900
+4900
+4900
+ed80
+ENDCHAR
+STARTCHAR n
+ENCODING 110
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+dc
+62
+42
+42
+42
+42
+e7
+ENDCHAR
+STARTCHAR o
+ENCODING 111
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+3c
+42
+81
+81
+81
+42
+3c
+ENDCHAR
+STARTCHAR p
+ENCODING 112
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+dc
+62
+41
+41
+41
+62
+5c
+40
+40
+f0
+ENDCHAR
+STARTCHAR q
+ENCODING 113
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+3b
+46
+82
+82
+82
+46
+3a
+02
+02
+0f
+ENDCHAR
+STARTCHAR r
+ENCODING 114
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+cc
+52
+60
+40
+40
+40
+f0
+ENDCHAR
+STARTCHAR s
+ENCODING 115
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+7c
+84
+80
+78
+04
+84
+f8
+ENDCHAR
+STARTCHAR t
+ENCODING 116
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 9 1 0
+BITMAP
+40
+40
+f8
+40
+40
+40
+40
+44
+38
+ENDCHAR
+STARTCHAR u
+ENCODING 117
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+c6
+42
+42
+42
+42
+46
+3b
+ENDCHAR
+STARTCHAR v
+ENCODING 118
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+e7
+42
+42
+24
+24
+18
+18
+ENDCHAR
+STARTCHAR w
+ENCODING 119
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 7 0 0
+BITMAP
+e380
+4100
+4900
+4900
+2a00
+3600
+3600
+ENDCHAR
+STARTCHAR x
+ENCODING 120
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+ee
+44
+28
+10
+28
+44
+ee
+ENDCHAR
+STARTCHAR y
+ENCODING 121
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+e7
+42
+42
+24
+24
+18
+08
+10
+10
+78
+ENDCHAR
+STARTCHAR z
+ENCODING 122
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 7 1 0
+BITMAP
+f8
+88
+10
+20
+40
+88
+f8
+ENDCHAR
+STARTCHAR braceleft
+ENCODING 123
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+20
+40
+40
+40
+40
+80
+40
+40
+40
+40
+40
+20
+ENDCHAR
+STARTCHAR bar
+ENCODING 124
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 11 4 -2
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+ENDCHAR
+STARTCHAR braceright
+ENCODING 125
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+80
+40
+40
+40
+40
+20
+40
+40
+40
+40
+40
+80
+ENDCHAR
+STARTCHAR asciitilde
+ENCODING 126
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 2 1 3
+BITMAP
+64
+98
+ENDCHAR
+STARTCHAR space
+ENCODING 160
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR Gamma
+ENCODING 161
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+42
+42
+40
+40
+40
+40
+40
+f0
+ENDCHAR
+STARTCHAR Delta
+ENCODING 162
+SWIDTH 288 0
+DWIDTH 9 0
+BBX 7 8 1 0
+BITMAP
+10
+10
+28
+28
+44
+44
+82
+fe
+ENDCHAR
+STARTCHAR Theta
+ENCODING 163
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+38
+44
+82
+82
+fe
+82
+82
+44
+38
+ENDCHAR
+STARTCHAR Lambda
+ENCODING 164
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 10 0 0
+BITMAP
+0800
+0800
+1C00
+3600
+3600
+6300
+6300
+C180
+C180
+E380
+ENDCHAR
+STARTCHAR Pi
+ENCODING 165
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 7 8 1 0
+BITMAP
+fe
+44
+44
+44
+44
+44
+44
+ee
+ENDCHAR
+STARTCHAR Sigma
+ENCODING 166
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+82
+40
+20
+10
+20
+40
+82
+fe
+ENDCHAR
+STARTCHAR Phi
+ENCODING 167
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+70
+20
+70
+a8
+a8
+a8
+70
+20
+70
+ENDCHAR
+STARTCHAR Psi
+ENCODING 168
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+38
+10
+92
+54
+54
+54
+38
+10
+38
+ENDCHAR
+STARTCHAR Omega
+ENCODING 169
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+38
+44
+82
+82
+82
+44
+28
+aa
+ee
+ENDCHAR
+STARTCHAR alpha
+ENCODING 170
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 8 6 0 0
+BITMAP
+39
+49
+8e
+8c
+8c
+76
+ENDCHAR
+STARTCHAR beta
+ENCODING 171
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 11 1 -3
+BITMAP
+1c
+22
+22
+4c
+42
+42
+44
+98
+80
+80
+00
+ENDCHAR
+STARTCHAR gamma
+ENCODING 172
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 7 9 1 -3
+BITMAP
+62
+94
+08
+08
+18
+18
+28
+28
+10
+ENDCHAR
+STARTCHAR delta
+ENCODING 173
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 10 2 0
+BITMAP
+38
+60
+40
+30
+78
+c8
+88
+90
+90
+60
+ENDCHAR
+
+STARTCHAR epsilon
+ENCODING 174
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 8 2 0
+BITMAP
+30
+48
+80
+60
+40
+80
+88
+70
+ENDCHAR
+STARTCHAR zeta
+ENCODING 175
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 6 13 1 -3
+BITMAP
+10
+1c
+20
+40
+40
+80
+80
+80
+c0
+70
+18
+18
+00
+ENDCHAR
+STARTCHAR eta
+ENCODING 176
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 6 9 1 -3
+BITMAP
+dc
+64
+44
+44
+88
+88
+08
+10
+10
+ENDCHAR
+STARTCHAR theta
+ENCODING 177
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+0c
+12
+12
+12
+ce
+24
+24
+48
+48
+70
+ENDCHAR
+STARTCHAR kappa
+ENCODING 178
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+ce
+50
+70
+50
+52
+8c
+ENDCHAR
+STARTCHAR lambda
+ENCODING 179
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+60
+30
+30
+18
+18
+2c
+2c
+46
+46
+83
+ENDCHAR
+STARTCHAR mu
+ENCODING 180
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 9 1 -3
+BITMAP
+22
+22
+44
+44
+44
+7e
+40
+80
+80
+ENDCHAR
+STARTCHAR nu
+ENCODING 181
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 6 6 1 0
+BITMAP
+64
+24
+28
+48
+50
+e0
+ENDCHAR
+STARTCHAR xi
+ENCODING 182
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 6 13 1 -3
+BITMAP
+10
+3c
+40
+40
+40
+38
+40
+80
+80
+f0
+08
+08
+10
+ENDCHAR
+STARTCHAR pi
+ENCODING 183
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+7e
+a8
+28
+28
+48
+48
+ENDCHAR
+STARTCHAR rho
+ENCODING 184
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 6 9 1 -3
+BITMAP
+1c
+24
+44
+44
+48
+70
+40
+40
+80
+ENDCHAR
+STARTCHAR sigma
+ENCODING 185
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+3e
+48
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR tau
+ENCODING 186
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 6 6 1 0
+BITMAP
+7c
+a0
+20
+20
+20
+c0
+ENDCHAR
+STARTCHAR varphi
+ENCODING 187
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 9 1 -3
+BITMAP
+4c
+92
+92
+a2
+a4
+78
+40
+40
+40
+ENDCHAR
+STARTCHAR chi
+ENCODING 188
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 8 9 0 -3
+BITMAP
+61
+32
+14
+18
+10
+10
+30
+48
+44
+ENDCHAR
+STARTCHAR psi
+ENCODING 189
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 11 1 -3
+BITMAP
+08
+48
+ca
+4a
+52
+54
+54
+38
+10
+00
+00
+ENDCHAR
+STARTCHAR omega
+ENCODING 190
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+42
+82
+92
+a2
+a4
+78
+ENDCHAR
+STARTCHAR not
+ENCODING 191
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 4 1 0
+BITMAP
+fe
+06
+06
+06
+ENDCHAR
+STARTCHAR and
+ENCODING 192
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+10
+28
+28
+44
+44
+82
+82
+ENDCHAR
+STARTCHAR or
+ENCODING 193
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+82
+82
+44
+44
+28
+28
+10
+ENDCHAR
+STARTCHAR forall
+ENCODING 194
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 11 1 -2
+BITMAP
+82
+82
+44
+7c
+44
+28
+28
+10
+10
+00
+00
+ENDCHAR
+STARTCHAR exists
+ENCODING 195
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+f8
+08
+08
+08
+f8
+08
+08
+08
+f8
+ENDCHAR
+STARTCHAR bigwedge
+ENCODING 196
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 11 1 -1
+BITMAP
+10
+10
+28
+28
+28
+44
+44
+44
+82
+82
+82
+ENDCHAR
+STARTCHAR lceil
+ENCODING 197
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+fe
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+ENDCHAR
+STARTCHAR rceil
+ENCODING 198
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+fe
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+ENDCHAR
+STARTCHAR lfloor
+ENCODING 199
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+fe
+ENDCHAR
+STARTCHAR rfloor
+ENCODING 200
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+fe
+ENDCHAR
+STARTCHAR llparenthesis
+ENCODING 201
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 12 3 -2
+BITMAP
+10
+30
+50
+90
+90
+90
+90
+90
+90
+50
+30
+10
+ENDCHAR
+STARTCHAR rrparenthesis
+ENCODING 202
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 12 2 -2
+BITMAP
+80
+c0
+a0
+90
+90
+90
+90
+90
+90
+a0
+c0
+80
+ENDCHAR
+STARTCHAR llbracket
+ENCODING 203
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+fe
+90
+90
+90
+90
+90
+90
+90
+90
+90
+90
+fe
+ENDCHAR
+STARTCHAR rrbracket
+ENCODING 204
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+FE
+12
+12
+12
+12
+12
+12
+12
+12
+12
+12
+FE
+ENDCHAR
+STARTCHAR emptyset
+ENCODING 205
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 13 0 -2
+BITMAP
+00
+00
+00
+00
+1d
+22
+45
+49
+51
+22
+5c
+00
+00
+ENDCHAR
+STARTCHAR in
+ENCODING 206
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 6 10 1 -3
+BITMAP
+3c
+40
+80
+f8
+80
+40
+3c
+00
+00
+00
+ENDCHAR
+STARTCHAR subseteq
+ENCODING 207
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 10 1 -2
+BITMAP
+7c
+80
+80
+80
+7c
+00
+7c
+00
+00
+00
+ENDCHAR
+STARTCHAR cap
+ENCODING 208
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+78
+cc
+84
+84
+84
+84
+84
+ENDCHAR
+STARTCHAR cup
+ENCODING 209
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+84
+84
+84
+84
+84
+cc
+78
+ENDCHAR
+STARTCHAR bigcap
+ENCODING 210
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+38
+44
+82
+82
+82
+82
+82
+82
+82
+82
+ENDCHAR
+STARTCHAR bigcup
+ENCODING 211
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+82
+82
+82
+82
+82
+82
+82
+82
+44
+38
+ENDCHAR
+STARTCHAR sqcap
+ENCODING 212
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+fc
+84
+84
+84
+84
+84
+84
+ENDCHAR
+STARTCHAR sqcup
+ENCODING 213
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+84
+84
+84
+84
+84
+84
+fc
+ENDCHAR
+STARTCHAR bigsqcap
+ENCODING 214
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+FE
+82
+82
+82
+82
+82
+82
+82
+82
+82
+ENDCHAR
+STARTCHAR bigsqcup
+ENCODING 215
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+82
+82
+82
+82
+82
+82
+82
+82
+82
+FE
+ENDCHAR
+STARTCHAR perp
+ENCODING 216
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+10
+10
+10
+fe
+ENDCHAR
+STARTCHAR doteq
+ENCODING 217
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+10
+00
+fe
+00
+fe
+ENDCHAR
+STARTCHAR equiv
+ENCODING 218
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 6 5 1 1
+BITMAP
+fc
+00
+fc
+00
+fc
+ENDCHAR
+STARTCHAR neq
+ENCODING 219
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 5 1 1
+BITMAP
+08
+fe
+10
+fe
+20
+ENDCHAR
+STARTCHAR sqsubset
+ENCODING 220
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 5 1 2
+BITMAP
+fc
+80
+80
+80
+fc
+ENDCHAR
+STARTCHAR sqsubseteq
+ENCODING 221
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 6 1 1
+BITMAP
+fc
+80
+80
+fc
+00
+fc
+ENDCHAR
+STARTCHAR prec
+ENCODING 222
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 2
+BITMAP
+02
+04
+18
+e0
+18
+04
+02
+ENDCHAR
+STARTCHAR preceq
+ENCODING 223
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+02
+04
+18
+e0
+18
+04
+02
+00
+fe
+ENDCHAR
+STARTCHAR succ
+ENCODING 224
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 2
+BITMAP
+80
+40
+30
+0e
+30
+40
+80
+ENDCHAR
+STARTCHAR succeq
+ENCODING 225
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+80
+40
+30
+0e
+30
+40
+80
+00
+fe
+ENDCHAR
+STARTCHAR sim
+ENCODING 226
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 3 1 3
+BITMAP
+60
+92
+0c
+ENDCHAR
+STARTCHAR simeq
+ENCODING 227
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+60
+92
+0c
+00
+fe
+ENDCHAR
+STARTCHAR le
+ENCODING 228
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+0c
+30
+c0
+30
+0c
+00
+00
+fc
+ENDCHAR
+STARTCHAR ge
+ENCODING 229
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+c0
+30
+0c
+30
+c0
+00
+00
+fc
+ENDCHAR
+STARTCHAR leftarrow
+ENCODING 230
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 5 0 2
+BITMAP
+3000
+6000
+ff80
+6000
+3000
+ENDCHAR
+STARTCHAR hline
+ENCODING 231
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 1 0 4
+BITMAP
+FF80
+ENDCHAR
+STARTCHAR rightarrow
+ENCODING 232
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 5 0 2
+BITMAP
+0c
+06
+ff
+06
+0c
+ENDCHAR
+STARTCHAR Leftarrow
+ENCODING 233
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 7 0 0
+BITMAP
+1800
+3000
+7f80
+c000
+7f80
+3000
+1800
+ENDCHAR
+STARTCHAR doublehline
+ENCODING 234
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 3 0 2
+BITMAP
+FF80
+0000
+FF80
+ENDCHAR
+STARTCHAR Rightarrow
+ENCODING 235
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+18
+0c
+fe
+03
+fe
+0c
+18
+ENDCHAR
+STARTCHAR twohead_rightarrow
+ENCODING 236
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 5 0 2
+BITMAP
+1200
+0900
+ff80
+0900
+1200
+ENDCHAR
+STARTCHAR mapsto
+ENCODING 237
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+88
+84
+fe
+84
+88
+ENDCHAR
+STARTCHAR leadsto
+ENCODING 238
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 5 0 2
+BITMAP
+04
+62
+93
+0e
+04
+ENDCHAR
+STARTCHAR uparrow
+ENCODING 239
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+20
+70
+a8
+20
+20
+20
+20
+20
+20
+ENDCHAR
+STARTCHAR downarrow
+ENCODING 240
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+20
+20
+20
+20
+20
+20
+a8
+70
+20
+ENDCHAR
+STARTCHAR not_in
+ENCODING 241
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 9 1 -1
+BITMAP
+08
+3c
+50
+90
+f8
+a0
+40
+7c
+80
+ENDCHAR
+STARTCHAR times
+ENCODING 242
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 6 1 0
+BITMAP
+84
+48
+30
+30
+48
+84
+ENDCHAR
+STARTCHAR oplus
+ENCODING 243
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+4900
+8880
+be80
+8880
+4900
+2200
+1c00
+ENDCHAR
+STARTCHAR ominus
+ENCODING 244
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 9 9 0 0 
+BITMAP
+1c00
+2200
+4100
+8080
+be80
+8080
+4100
+2200
+1c00
+ENDCHAR
+STARTCHAR otimes
+ENCODING 245
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+6300
+9480
+8880
+9480
+6300
+2200
+1c00
+ENDCHAR
+STARTCHAR oslash
+ENCODING 246
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 9 0 0 
+BITMAP
+1c00
+2200
+4300
+8480
+8880
+9080
+6100
+2200
+1c00
+ENDCHAR
+STARTCHAR natural
+ENCODING 247
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 9 2 0
+BITMAP
+80
+90
+b0
+d0
+90
+b0
+d0
+90
+10
+ENDCHAR
+STARTCHAR infinity
+ENCODING 248
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+44
+aa
+92
+aa
+44
+ENDCHAR
+STARTCHAR Box
+ENCODING 249
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 5 2 1
+BITMAP
+f8
+88
+88
+88
+f8
+ENDCHAR
+STARTCHAR Diamond
+ENCODING 250
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+28
+44
+82
+44
+28
+10
+ENDCHAR
+STARTCHAR circ
+ENCODING 251
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 5 2 2
+BITMAP
+70
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR bullet
+ENCODING 252
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 5 2 2
+BITMAP
+70
+f8
+f8
+f8
+70
+ENDCHAR
+STARTCHAR parallel
+ENCODING 253
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 12 1 -2
+BITMAP
+14
+14
+14
+14
+14
+14
+14
+14
+14
+14
+14
+14
+ENDCHAR
+STARTCHAR surd
+ENCODING 254
+SWIDTH 0 0
+DWIDTH 9 0
+BBX 7 8 1 0
+BITMAP
+06
+04
+04
+c8
+48
+50
+30
+20
+ENDCHAR
+STARTCHAR copyright
+ENCODING 255
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+5d00
+a080
+a080
+a080
+5d00
+2200
+1c00
+ENDCHAR
+ENDFONT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/oldisacr14.bdf	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,2945 @@
+STARTFONT 2.1
+COMMENT
+COMMENT  Copyright 1984, 1987 Adobe Systems, Inc.
+COMMENT  Portions Copyright 1988 Digital Equipment Corporation
+COMMENT  Portions Copyright 1993 TU Muenchen, Germany
+COMMENT
+COMMENT  Adobe is a registered trademark of Adobe Systems, Inc.  Permission
+COMMENT  to use these trademarks is hereby granted only in association with the
+COMMENT  images described in this file.
+COMMENT
+COMMENT  Permission to use, copy, modify, and distribute this software and
+COMMENT  its documentation for any purpose and without fee is hereby granted,
+COMMENT  provided that the above copyright notices appear in all copies and
+COMMENT  that both those copyright notices and this permission notice appear
+COMMENT  in supporting documentation, and that the names of Adobe Systems,
+COMMENT  Digital Equipment Corporation, and TU Muenchen not be used in
+COMMENT  advertising or publicity pertaining to distribution of the software
+COMMENT  without specific, written prior permission.  Adobe Systems, Digital
+COMMENT  Equipment Corporation, and TU Muenchen  make no representations about
+COMMENT  the suitability of this software for any purpose.  It is provided "as
+COMMENT  is" without express or implied warranty.
+COMMENT
+COMMENT  ADOBE SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN DISCLAIM
+COMMENT  ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL IMPLIED
+COMMENT  WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO EVENT SHALL ADOBE
+COMMENT  SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN BE LIABLE FOR 
+COMMENT  ANY SPECIAL, INDIRECT OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+COMMENT  WHATSOEVE RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+COMMENT  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT 
+COMMENT  OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+FONT oldisacr14
+SIZE 14 75 75
+FONTBOUNDINGBOX 9 14 4 -3
+STARTPROPERTIES 22
+FONTNAME_REGISTRY ""
+FAMILY_NAME "Isabelle"
+FOUNDRY ""
+WEIGHT_NAME "Medium"
+SLANT "R"
+SETWIDTH_NAME "Normal"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 14
+POINT_SIZE 140
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "M"
+AVERAGE_WIDTH 90
+CHARSET_REGISTRY ""
+CHARSET_ENCODING "1"
+CHARSET_COLLECTIONS ""
+FULL_NAME "OldIsabelle14"
+COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1995 TU Muenchen"
+FONT_ASCENT 11
+FONT_DESCENT 3
+CAP_HEIGHT 9
+X_HEIGHT 7
+ENDPROPERTIES
+CHARS 191
+STARTCHAR space
+ENCODING 32
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR exclam
+ENCODING 33
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 10 3 0
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+00
+00
+80
+ENDCHAR
+STARTCHAR quotedbl
+ENCODING 34
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 4 2 5
+BITMAP
+90
+90
+90
+90
+ENDCHAR
+STARTCHAR numbersign
+ENCODING 35
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+50
+50
+50
+f8
+50
+f8
+50
+50
+50
+ENDCHAR
+STARTCHAR dollar
+ENCODING 36
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 13 2 -2
+BITMAP
+20
+20
+78
+88
+80
+c0
+30
+08
+88
+f0
+20
+20
+20
+ENDCHAR
+STARTCHAR percent
+ENCODING 37
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+60
+90
+90
+66
+18
+30
+cc
+12
+12
+0c
+ENDCHAR
+STARTCHAR ampersand
+ENCODING 38
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+38
+48
+40
+40
+a8
+90
+98
+64
+ENDCHAR
+STARTCHAR quoteright
+ENCODING 39
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 5
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR parenleft
+ENCODING 40
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+20
+40
+40
+80
+80
+80
+80
+80
+80
+40
+40
+20
+ENDCHAR
+STARTCHAR parenright
+ENCODING 41
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+80
+40
+40
+20
+20
+20
+20
+20
+20
+40
+40
+80
+ENDCHAR
+STARTCHAR asterisk
+ENCODING 42
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 6 1 3
+BITMAP
+20
+20
+f8
+20
+50
+88
+ENDCHAR
+STARTCHAR plus
+ENCODING 43
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+fe
+10
+10
+10
+ENDCHAR
+STARTCHAR comma
+ENCODING 44
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 -2
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR minus
+ENCODING 45
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 1 1 4
+BITMAP
+fe
+ENDCHAR
+STARTCHAR period
+ENCODING 46
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 2 2 3 0
+BITMAP
+c0
+c0
+ENDCHAR
+STARTCHAR slash
+ENCODING 47
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+04
+08
+08
+10
+10
+20
+20
+40
+40
+80
+80
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+84
+84
+84
+84
+84
+84
+78
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 10 1 0
+BITMAP
+20
+60
+a0
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+04
+08
+10
+20
+40
+84
+fc
+ENDCHAR
<