...
authorwenzelm
Mon, 02 Jul 2001 20:55:43 +0200
changeset 11390 735bf767833a
parent 11389 55e2aef8909b
child 11391 e8638d07fdee
...
src/Tools/8bit/IMPORTANT
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/lex.x
src/Tools/8bit/c-sources/a2isa/main.c
src/Tools/8bit/c-sources/a2isa/xlex.x
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/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/Makefile
src/Tools/8bit/doc/Set2.thy
src/Tools/8bit/doc/Set2_a.thy
src/Tools/8bit/doc/Set2_g.thy
src/Tools/8bit/doc/Set2g.thy
src/Tools/8bit/doc/Set2x.thy
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/isabelle14.bdf
src/Tools/8bit/fonts/isabelle24.bdf
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/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/Up3.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/mk
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
--- a/src/Tools/8bit/IMPORTANT	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-
-IMPORTANT NOTE:
-===============
-
-The 8bit package has 'contrib' status. It will disappear someday
-without prior notice.  Use at your own risk.
--- a/src/Tools/8bit/Makefile	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,406 +0,0 @@
-###############################################
-# 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/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'
-
-# name of GNU make utility: `make' on linux box; `gmake' on solaris
-#GMAKE=make
-GMAKE=gmake
-
-#keycode for Super_L  (= left Meta)
-SUPER_L=127
-
-#keycode for Hyper_R (= right Meta)
-HYPER_R=129
-
-CONFIGFILES = config/Makefile config/key-table.inp config/conv-tables.inp
-
-#path stem to isabelle source, used by patcher
-STEM = /usr/wiss/oheimb/isabelle/
-
-###############################################
-# 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 manual a2isa bin/isa2latex bin/a2isa bin/ax2isa\
-	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\
-	isa-patches/HOL/add-HOL.cfg isa-patches/HOL/clean-HOL.cfg\
-	isa-patches/HOL/extract-HOL.cfg\
-	isa-patches/HOLCF/add-HOLCF.cfg isa-patches/HOLCF/clean-HOLCF.cfg\
-	isa-patches/HOLCF/extract-HOLCF.cfg
-
-# ----------------------------------------------------
-
-clean:
-#	cd bin; rm -f *2isa codetable gen-* isa* patcher
-	cd c-sources/a2isa; $(GMAKE) clean
-	cd c-sources/isa2latex; $(GMAKE) clean
-	cd doc; $(GMAKE) clean
-
-###############################################
-# 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;" \
-		-e "s#^GMAKE\s*=.*#GMAKE= $(GMAKE)#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
-	@echo $(CONV_SOURCE_DIR)
-
-#######      Generators        
-
-# ----------------------------------------------------
-
-bin/gen-isa2latex: Makefile #perl/generators/gen-isa2latex.pl
-	@echo "configuring gen-isa2latex"
-	@cd perl/generators;\
-	$(PERL) -pi \
-		-e "s#GMAKE\s*=.*#GMAKE= \"$(GMAKE)\";#g;" \
-		-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
-	@rm -f doc/isa2latex.sty;\
-	ln -s ../latex/isa2latex.sty doc/isa2latex.sty
-
-
-#######      Converter        
-
-# ----------------------------------------------------
-
-#isa2latex, editor support, font documentation:
-configuration:
-	@cd config; $(GMAKE)
-
-manual:
-	@cd doc; $(GMAKE) manual.dvi
-
-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
-
-bin/ax2isa: c-sources/a2isa/ax2isa
-	@echo "installing ax2isa"
-	@rm -f bin/ax2isa;\
-	ln -s ../c-sources/a2isa/ax2isa bin/ax2isa
-
-#######      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
-
-isa-patches/HOL/add-HOL.cfg: Makefile
-	@cd isa-patches/HOL;\
-	$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" add-HOL.cfg
-isa-patches/HOL/clean-HOL.cfg: Makefile
-	@cd isa-patches/HOL;\
-	$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" clean-HOL.cfg
-isa-patches/HOL/extract-HOL.cfg: Makefile
-	@cd isa-patches/HOL;\
-	$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" extract-HOL.cfg
-isa-patches/HOLCF/add-HOLCF.cfg: Makefile
-	@cd isa-patches/HOLCF;\
-	$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" add-HOLCF.cfg
-isa-patches/HOLCF/clean-HOLCF.cfg: Makefile
-	@cd isa-patches/HOLCF;\
-	$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" clean-HOLCF.cfg
-isa-patches/HOLCF/extract-HOLCF.cfg: Makefile
-	@cd isa-patches/HOLCF;\
-	$(PERL) -pi -e "s#^STEM\s*\".*#STEM \"$(STEM)\"#g;" extract-HOLCF.cfg
-
-# ----------------------------------------------------
-
--- a/src/Tools/8bit/README	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-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 mk
-(after further changes, if may be sufficient to call gmake)
-
-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
--- a/src/Tools/8bit/axe/isaaxe	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-#!/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 "isabelle14" -title "IsaAxe" -geometry 80x40 -xrm "\
-*fontMenu.label:    Fonts" -xrm "\
-*FontList: Isa14:isabelle14 Isa24:isabelle24" -xrm "\
-*Axe*ed.translations: #override\
-	!Mod2 <Key>space:		insert-string(0xa0)  \n\
-	!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\
-	!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\
-	!Mod4 <Key>i:		insert-string(0xe7) insert-string(0xe8)  \n\
-	!Mod4 Shift <Key>i:		insert-string(0xea) insert-string(0xeb)  \n\
-	!Mod4 Shift <Key>m:		insert-string(0xe8)  \n\
-	!Mod4 <Key>m:		insert-string(0xeb)  \n\
-	!Mod4 Shift <Key>n:		insert-string(0xf7)  \n\
-	!Mod4 <Key>x:		insert-string(0xf2)  \n\
-	! <Key>F2:		insert-string(0xe4)  \n\
-	! <Key>F3:		insert-string(0xdd)  \n\
-	! <Key>F4:		insert-string(0xcf)  \n\
-	! <Key>F5:		insert-string(0xce)  \n\
-	! <Key>F6:		insert-string(0xf1)  \n\
-	! <Key>F7:		insert-string(0xe5)  \n\
-	! <Key>F8:		insert-string(0xda)  \n\
-	! <Key>F9:		insert-string(0xc4)  \n\
-	! <Key>F10:		insert-string(0xcb)  \n\
-	! <Key>F11:		insert-string(0xcc)  \n\
-	! <Key>F12:		insert-string(0xea) insert-string(0xeb)  \n\
-	!Shift <Key>F1:		insert-string(0xe9)  \n\
-	!Shift <Key>F2:		insert-string(0xea)  \n\
-	!Shift <Key>F3:		insert-string(0xeb)  \n\
-	!Shift <Key>F4:		insert-string(0xe9) insert-string(0xeb)  \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(0xca)  \n\
-	!Shift <Key>F10:		insert-string(0xc9)  \n\
-	!Ctrl <Key>F1:		insert-string(0xe6)  \n\
-	!Ctrl <Key>F2:		insert-string(0xe7)  \n\
-	!Ctrl <Key>F3:		insert-string(0xe8)  \n\
-	!Ctrl <Key>F4:		insert-string(0xe6) insert-string(0xe8)  \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(0xfd)  \n\
-	!Ctrl <Key>F10:		insert-string(0xcd)  \n\
-	!Mod2 <Key>F1:		insert-string(0xed)  \n\
-	!Mod2 <Key>F2:		insert-string(0xee)  \n\
-	!Mod2 <Key>F3:		insert-string(0xef)  \n\
-	!Mod2 <Key>F4:		insert-string(0xf0)  \n\
-	!Mod2 <Key>F5:		insert-string(0xd4)  \n\
-	!Mod2 <Key>F6:		insert-string(0xd5)  \n\
-	!Mod2 <Key>F7:		insert-string(0xd6)  \n\
-	!Mod2 <Key>F8:		insert-string(0xd7)  \n\
-	!Mod2 <Key>F9:		insert-string(0xdc)  \n\
-	!Mod2 <Key>F10:		insert-string(0xf8)  \n\
-	!Mod4 <Key>F1:		insert-string(0xf9)  \n\
-	!Mod4 <Key>F2:		insert-string(0xfa)  \n\
-	!Mod4 <Key>F3:		insert-string(0xfb)  \n\
-	!Mod4 <Key>F4:		insert-string(0xfc)  \n\
-	!Mod4 <Key>F5:		insert-string(0xd0)  \n\
-	!Mod4 <Key>F6:		insert-string(0xd1)  \n\
-	!Mod4 <Key>F7:		insert-string(0xd2)  \n\
-	!Mod4 <Key>F8:		insert-string(0xd3)  \n\
-	!Mod4 <Key>F9:		insert-string(0xf7)  \n\
-	!Mod4 <Key>F10:		insert-string(0xec)  \n\
-	!Mod4 <Key>F11:		insert-string(0xfe)  \n\
-	!Mod4 <Key>F12:		insert-string(0xff)  \
-" $*
--- a/src/Tools/8bit/c-sources/a2isa/Makefile	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-###############################################
-# Title:      Tools/8bit/c-sources/a2isa/Makefile
-# ID:         $Id$
-# Author:     David von Oheimb
-# Copyright   1996 TU Muenchen
-#
-# Makefile for Isabelle ASCII to 8bit converter
-################################################
-
-AOBJECTS  = main.o  lex.o
-AXOBJECTS = main.o xlex.o
-
-CC = gcc
-
-.SUFFIXES: $(SUFFIXES) .x
-
-.x.o:
-	flex $<; $(CC) -c -o $@ lex.yy.c
-
-# ----------------------------------------------------
-
-all: a2isa ax2isa
-
-a2isa:  $(AOBJECTS)
-	$(CC) -o a2isa $(AOBJECTS); strip a2isa
-
-ax2isa: $(AXOBJECTS)
-	$(CC) -o ax2isa $(AXOBJECTS); strip ax2isa
-
-#lex.o: lex.x
-#	flex lex.x; $(CC) -c -o lex.o lex.yy.c
-
-# ----------------------------------------------------
-
-clean:
-	@rm -f *.o lex.yy.c
--- a/src/Tools/8bit/c-sources/a2isa/lex.x	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-/*  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("");
-::		put("");
-'a		put("");
-'b		put("");
-'c		put("");
-'r		put("");
-'s		put("");
-'t		put("");
-
-   /* HOL */
-\ \*\ 		put("  ");
-@[ A-Za-z]	{ *yytext=''; put(yytext); }
-\ &\ 		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("");
-  /*
-  > "{}"		"\mbox{$\emptyset$}"
-# > "<="		"\mbox{$\subseteq$}"
-  */
-\ Int\ 		put("");
-\ Un\ 		put("");
-Inter\ 		put("");
-Union\ 		put("");
-
-   /* Nat */
-LEAST\ 		put("");
-
-   /* HOLCF */
-->		put("");
-\*\*		put("");
-\+\+		put("");
-
-\<\<\|		put("<<|");
-\<\|		put("<|");
-\<\<		put("");
-LAM\ 		put("");
-lub\ 		put("");
-UU		put("");
-
-  /* misc */
-\|-put("");
-\|=		put("");
-
-  /*
-  >  "\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$}" 
-  >  "\sqcap\ "		"\mbox{$\sqcap$}" 
-  >  "\sqcup\ "		"\mbox{$\sqcup$}"
-  >  "\cdot\ "		"\mbox{$\cdot$}"
-
-glb\ 		put("");
-===		put("");
-
-  /*
-  >  "\sqsubset\ "	"\mbox{$\sqsubset$}" 
-  >  "\prec\ "		"\mbox{$\prec$}" 
-  >  "\preceq\ "	"\mbox{$\preceq$}" 
-  >  "\Succ\ "		"\mbox{$\succ$}" 
-  >  "\approx\ "	"\mbox{$\approx$}" 
-  >  "\sim\ "		"\mbox{$\sim$}" 
-  >  "\simeq\ "		"\mbox{$\simeq$}" 
-  >  "\le\ "		"\mbox{$\le$}" 
-  >  "\ge\ "		"\mbox{$\ge$}" 
-  */
-
-\<==		put("");
-\<=>		put("");
-\<--		put("");
-\<->		put("");
-\<-		put("");
-
-  /*
-  >  "\frown\ "		"\mbox{$\frown$}" 
-  >  "\mapsto\ "	"\mbox{$\mapsto$}" 
-  >  "\leadsto\ "	"\mbox{$\leadsto$}" 
-  >  "\uparrow\ "	"\mbox{$\uparrow$}" 
-  >  "\downarrow\ "	"\mbox{$\downarrow$}" 
-
-  >  "\ominus\ "	"\mbox{$\varominus$}" 
-  >  "\oslash\ "	"\mbox{$\varoslash$}" 
-  >  "\subset\ "	"\mbox{$\subset$}" 
-  >  "\infty\ "		"\mbox{$\infty$}" 
-  >  "\Box\ "		"\mbox{$\Box$}" 
-  >  "\Diamond\ "	"\mbox{$\Diamond$}" 
-  >  "\circ\ "		"\mbox{$\circ$}" 
-  >  "\bullet\ "	"\mbox{$\bullet$}" 
-  >  "||"		"\mbox{$\parallel$}" 
-  >  "\tick\ "		"\mbox{$\surd$}" 
-  >  "\filter\ "	"\mbox{\copyright}"
-  */
-}
-%%
--- a/src/Tools/8bit/c-sources/a2isa/main.c	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-/*  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);
-}
-
-
--- a/src/Tools/8bit/c-sources/a2isa/xlex.x	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-/*  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;
-
-\\I@			{ ECHO; BEGIN(STRING); }
-.			{ ECHO; }
-<STRING>\\I@		{ 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("");
-::		put("");
-'a		put("");
-'b		put("");
-'c		put("");
-'r		put("");
-'s		put("");
-'t		put("");
-
-   /* HOL */
-\ \*\ 		put("  ");
-@[ A-Za-z]	{ *yytext=''; put(yytext); }
-\ &\ 		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("");
-  /*
-  > "{}"		"\mbox{$\emptyset$}"
-# > "<="		"\mbox{$\subseteq$}"
-  */
-\ Int\ 		put("");
-\ Un\ 		put("");
-Inter\ 		put("");
-Union\ 		put("");
-
-   /* Nat */
-LEAST\ 		put("");
-
-   /* HOLCF */
-->		put("");
-\*\*		put("");
-\+\+		put("");
-
-\<\<\|		put("<<|");
-\<\|		put("<|");
-\<\<		put("");
-LAM\ 		put("");
-lub\ 		put("");
-UU		put("");
-
-  /* misc */
-\|-		put("");
-\|=		put("");
-
-  /*
-  >  "\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$}" 
-  >  "\sqcap\ "		"\mbox{$\sqcap$}" 
-  >  "\sqcup\ "		"\mbox{$\sqcup$}"
-  >  "\cdot\ "		"\mbox{$\cdot$}"
-
-glb\ 		put("");
-===		put("");
-
-  /*
-  >  "\sqsubset\ "	"\mbox{$\sqsubset$}" 
-  >  "\prec\ "		"\mbox{$\prec$}" 
-  >  "\preceq\ "	"\mbox{$\preceq$}" 
-  >  "\Succ\ "		"\mbox{$\succ$}" 
-  >  "\approx\ "	"\mbox{$\approx$}" 
-  >  "\sim\ "		"\mbox{$\sim$}" 
-  >  "\simeq\ "		"\mbox{$\simeq$}" 
-  >  "\le\ "		"\mbox{$\le$}" 
-  >  "\ge\ "		"\mbox{$\ge$}" 
-  */
-
-\<==		put("");
-\<=>		put("");
-\<--		put("");
-\<->		put("");
-\<-		put("");
-
-  /*
-  >  "\frown\ "		"\mbox{$\frown$}" 
-  >  "\mapsto\ "	"\mbox{$\mapsto$}" 
-  >  "\leadsto\ "	"\mbox{$\leadsto$}" 
-  >  "\uparrow\ "	"\mbox{$\uparrow$}" 
-  >  "\downarrow\ "	"\mbox{$\downarrow$}" 
-
-  >  "\ominus\ "	"\mbox{$\varominus$}" 
-  >  "\oslash\ "	"\mbox{$\varoslash$}" 
-  >  "\subset\ "	"\mbox{$\subset$}" 
-  >  "\infty\ "		"\mbox{$\infty$}" 
-  >  "\Box\ "		"\mbox{$\Box$}" 
-  >  "\Diamond\ "	"\mbox{$\Diamond$}" 
-  >  "\circ\ "		"\mbox{$\circ$}" 
-  >  "\bullet\ "	"\mbox{$\bullet$}" 
-  >  "||"		"\mbox{$\parallel$}" 
-  >  "\tick\ "		"\mbox{$\surd$}" 
-  >  "\filter\ "	"\mbox{\copyright}"
-  */
-}
-%%
--- a/src/Tools/8bit/c-sources/isa2latex/Makefile	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-###############################################
-# 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 >/tmp/tmp.c ; 
-	$(CC) -c -o conv-lex.o /tmp/tmp.c ;
-	rm -f /tmp/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 
--- a/src/Tools/8bit/c-sources/isa2latex/conv-defs.h	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-/*
- * 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  160
-#define END_HI_TABLE    255
-#define SEQ_TABLE       29
-/* END gen-isa2latex */
-
--- a/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,350 +0,0 @@
-/*  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_beg0[], isa_env_beg1[], 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, 
-			  (yytext[3]=='@' ? "\\mbox{\\isainline[\\isamodify]{"
-					  : "\\mbox{\\isainline{")); }
-<LATEX>\\I@isa@?[ \t]*\n? { BEGIN_ISA; inline_mode=FALSE; fprintf(foutput, 
-				(yytext[6]=='@' ? isa_env_beg1
-						: isa_env_beg0)); reset_tabs(); 
-			  if (yytext[strlen(yytext)-1] == '\n')
-			  { fprintf(foutput, "\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 (yytext[0] == '\n')
-			    { fprintf(foutput, "\n"); lineno++; };
-			  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"); }
-			  }
-			}
-<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>\ \             	put((char)160,FALSE,0);
-<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>\\cdot          	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><:              	put((char)222,FALSE,0);
-<ISAA><=:             	put((char)223,FALSE,0);
-<ISAA>:>              	put((char)224,FALSE,0);
-<ISAA>~~              	put((char)225,FALSE,0);
-<ISAA>\\sim\          	put((char)226,FALSE,0);
-<ISAA>\\simeq         	put((char)227,FALSE,0);
-<ISAA><=              	put((char)228,FALSE,0);
-<ISAA>::              	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>\\frown         	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>\+\+            	put((char)243,FALSE,0);
-<ISAA>\\ominus        	put((char)244,FALSE,0);
-<ISAA>\*\*            	put((char)245,FALSE,0);
-<ISAA>\\oslash        	put((char)246,FALSE,0);
-<ISAA>\\subset        	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);
-<ISA,ISAA>^and            	put((char)32,TRUE,11);
-<ISAA>^@and                	put((char)32,TRUE,11);
-<ISA,ISAA>^arities        	put((char)32,TRUE,12);
-<ISAA>^@arities            	put((char)32,TRUE,12);
-<ISA,ISAA>^axclass        	put((char)32,TRUE,13);
-<ISAA>^@axclass            	put((char)32,TRUE,13);
-<ISA,ISAA>^constdefs      	put((char)32,TRUE,14);
-<ISAA>^@constdefs          	put((char)32,TRUE,14);
-<ISA,ISAA>^consts         	put((char)32,TRUE,15);
-<ISAA>^@consts             	put((char)32,TRUE,15);
-<ISA,ISAA>^datatype       	put((char)32,TRUE,16);
-<ISAA>^@datatype           	put((char)32,TRUE,16);
-<ISA,ISAA>^defs           	put((char)32,TRUE,17);
-<ISAA>^@defs               	put((char)32,TRUE,17);
-<ISA,ISAA>^domain         	put((char)32,TRUE,18);
-<ISAA>^@domain             	put((char)32,TRUE,18);
-<ISA,ISAA>^end            	put((char)32,TRUE,19);
-<ISAA>^@end                	put((char)32,TRUE,19);
-<ISA,ISAA>^inductive      	put((char)32,TRUE,20);
-<ISAA>^@inductive          	put((char)32,TRUE,20);
-<ISA,ISAA>^instance       	put((char)32,TRUE,21);
-<ISAA>^@instance           	put((char)32,TRUE,21);
-<ISA,ISAA>^primrec        	put((char)32,TRUE,22);
-<ISAA>^@primrec            	put((char)32,TRUE,22);
-<ISA,ISAA>^recdef         	put((char)32,TRUE,23);
-<ISAA>^@recdef             	put((char)32,TRUE,23);
-<ISA,ISAA>^rules          	put((char)32,TRUE,24);
-<ISAA>^@rules              	put((char)32,TRUE,24);
-<ISA,ISAA>^syntax         	put((char)32,TRUE,25);
-<ISAA>^@syntax             	put((char)32,TRUE,25);
-<ISA,ISAA>^translations   	put((char)32,TRUE,26);
-<ISAA>^@translations       	put((char)32,TRUE,26);
-<ISA,ISAA>^typedef        	put((char)32,TRUE,27);
-<ISAA>^@typedef            	put((char)32,TRUE,27);
-<ISA,ISAA>^types          	put((char)32,TRUE,28);
-<ISAA>^@types              	put((char)32,TRUE,28);
-  /* 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;
-  char s[100];
-  extern char *translateHi(int ch, int code);
-
-    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... */
-       strcpy(s, translateHi(c, destCode));
-       i = strlen(s);
-       if((unsigned char)c != 0xa0 &&
-	  i >= 2 && s[i-2] == '\\' && s[i-1] == ' ' && (yytext[0] & 0x80))
-	 s[i-2] ='\0';
-       fprintf(foutput, "%s", s);
-        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 */
-}       
-
-
-
-
-
-
--- a/src/Tools/8bit/c-sources/isa2latex/conv-main.c	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-/*  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_beg0[200],      /* latex command to begin isa environment */
-     isa_env_beg1[200];
-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[]{article}\n");
-      fprintf(foutput, 
-	 "\\usepackage{latexsym,amssymb,isa2latex}\n");
-    } else {
-      fprintf(foutput, 
-	 "\\documentstyle[10pt,latexsym,amssymb,isa2latex]{article}\n");
-    }
-      fprintf(foutput, "\\topmargin-8ex\n"
-	               "\\oddsidemargin0ex\n"
-	               "\\textheight158ex\n"
-	               "\\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{-1.2ex}\n");
-  strcpy(isa_env_end, "\n\\end{tabbing}}");
-   */
-  strcpy(isa_env_beg0, "{\\isabegin{}\\noindent ");
-  strcpy(isa_env_beg1, "{\\isabegin{\\isamodify}\\noindent ");
-  strcpy(isa_env_end , "\\isaend}\\noindent ");
-  
-  if (convMode == STANDALONE || (convMode == INCLUDE) && (destCode != TO_7bit))
-    fprintf(foutput, isa_env_beg0);
-
-  /*
-   * start the conversion: use lexer in all modes to do the job.
-   */
-  
-  reset_tabs();
-  yylex();
-
-  /*
-   * output footers
-   */
-
-  if(convMode == STANDALONE || (convMode == INCLUDE) && (destCode != TO_7bit))
-    fprintf(foutput, isa_env_end);
-
-  if(convMode == STANDALONE) 
-      fprintf(foutput, "\\end{document}\n");
-  return(0);
-}
-
-
--- a/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,272 +0,0 @@
-/*
- * 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{}",
-   "\\#",
-   "\\$",
-   "\\%",
-   "\\&",
-   "'",
-   "(",
-   ")",
-   "{*}",
-   "+",
-   ",",
-   "-",
-   ".",
-   "/",
-   "0",
-   "1",
-   "2",
-   "3",
-   "4",
-   "5",
-   "6",
-   "7",
-   "8",
-   "9",
-   ":",
-   ";",
-   "<",
-   "=",
-   ">",
-   "?",
-   "@",
-   "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",
-   "[",
-   "\\ttbackslash{}",
-   "]",
-   "\\^{}",
-   "{\\_\\hspace{.344ex}}",
-   "`",
-   "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",
-   "\\{",
-   "|",
-   "\\}",
-   "\\tttilde{}"
-};
-/* 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$}"},
-   {"@"           ,"\\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$}"},
-   {"\\p"         ,"\\mbox{$\\pi$}"},
-   {"'r"          ,"\\mbox{$\\rho$}"},
-   {"'s"          ,"\\mbox{$\\sigma$}"},
-   {"'t"          ,"\\mbox{$\\tau$}"},
-   {"\\varphi"    ,"\\mbox{$\\varphi$}"},
-   {"\\chi"       ,"\\mbox{$\\chi$}"},
-   {"\\psi"       ,"\\mbox{$\\psi$}"},
-   {"\\omega"     ,"\\mbox{$\\omega$}"},
-   {"~ "          ,"\\mbox{$\\hspace{-.33ex}\\neg$}"},
-   {"& "          ,"\\mbox{$\\hspace{-.185ex}\\wedge\\hspace{-.185ex}$}\\ "},
-   {"| "          ,"\\mbox{$\\hspace{-.185ex}\\vee\\hspace{-.185ex}$}\\ "},
-   {"!"           ,"\\mbox{$\\hspace{-.07ex}\\forall$}"},
-   {"? "          ,"\\mbox{$\\hspace{-.07ex}\\exists$}"},
-   {"!!"          ,"\\mbox{$\\bigwedge$}"},
-   {"\\lceil"     ,"\\mbox{$\\lceil$}"},
-   {"\\rceil"     ,"\\mbox{$\\rceil$}"},
-   {"\\lfloor"    ,"\\mbox{$\\lfloor$}"},
-   {"\\rfloor"    ,"\\mbox{$\\rfloor$}"},
-   {"|-"          ,"\\mbox{$\\hspace{.49ex}\\vdash\\hspace{.49ex}$}"},
-   {"|="          ,"\\mbox{$\\models$}"},
-   {"[|"          ,"\\mbox{$[\\![\\hspace{.32ex}$}"},
-   {"|]"          ,"\\mbox{$\\hspace{.32ex}]\\!]$}"},
-   {"."           ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"},
-   {":"           ,"\\mbox{$\\hspace{.445ex}\\in\\hspace{.445ex}$}"},
-   {" <= "        ,"\\mbox{$\\subseteq$}"},
-   {" Int "       ,"\\mbox{$\\cap$}"},
-   {" Un "        ,"\\mbox{$\\cup$}"},
-   {"INT "        ,"\\mbox{$\\bigcap$}"},
-   {"UN "         ,"\\mbox{$\\bigcup$}"},
-   {"\\sqcap"     ,"\\mbox{$\\hspace{.29ex}\\sqcap\\hspace{.29ex}$}"},
-   {"\\sqcup"     ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"},
-   {"glb "        ,"\\mbox{$\\overline{|\\,\\,|}$}"},
-   {"LUB "        ,"\\mbox{$\\bigsqcup$}"},
-   {"UU"          ,"\\mbox{$\\hspace{-.29ex}\\bot\\hspace{-.29ex}$}"},
-   {".="          ,"\\mbox{$\\doteq$}"},
-   {"=="          ,"\\mbox{$\\hspace{.29ex}\\equiv\\hspace{.29ex}$}"},
-   {"~="          ,"\\mbox{$\\hspace{-.34ex}\\not\\hspace{-.3ex}\\mbox{=}$}"},
-   {"\\sqsubset"  ,"\\mbox{$\\hspace{.29ex}\\sqsubset\\hspace{.29ex}$}"},
-   {"<<"          ,"\\mbox{$\\hspace{.29ex}\\sqsubseteq\\hspace{.29ex}$}"},
-   {"<:"          ,"\\mbox{$\\hspace{.29ex}\\prec\\hspace{.29ex}$}\\ "},
-   {"<=:"         ,"\\mbox{$\\hspace{.29ex}\\preceq\\hspace{.29ex}$}"},
-   {":>"          ,"\\mbox{$\\hspace{.29ex}\\succ\\hspace{.29ex}$}\\ "},
-   {"~~"          ,"\\mbox{$\\hspace{.29ex}\\approx\\hspace{.29ex}$}"},
-   {"\\sim "      ,"\\mbox{$\\hspace{.29ex}\\sim\\hspace{.29ex}$}\\ "},
-   {"\\simeq"     ,"\\mbox{$\\hspace{.29ex}\\simeq\\hspace{.29ex}$}"},
-   {"<="          ,"\\mbox{$\\hspace{.29ex}\\le\\hspace{.29ex}$}"},
-   {"::"          ,"\\mbox{$:\\hspace{-.07ex}:$}"},
-   {"<-"          ,"\\mbox{$\\leftarrow$}"},
-   {"-"           ,"\\mbox{$-$}"},
-   {"->"          ,"\\mbox{$\\rightarrow$}"},
-   {"<="          ,"\\mbox{$\\Leftarrow$}"},
-   {"="           ,"\\mbox{$=$}"},
-   {"=>"          ,"\\mbox{$\\hspace{.12ex}\\Rightarrow$}"},
-   {"\\frown"     ,"\\mbox{$\\frown$}"},
-   {"|->"         ,"\\mbox{$\\mapsto$}"},
-   {"~>"          ,"\\mbox{$\\hspace{.05ex}\\leadsto$}"},
-   {"\\uparrow"   ,"\\mbox{$\\uparrow$}"},
-   {"\\downarrow" ,"\\mbox{$\\downarrow$}"},
-   {"~:"          ,"\\mbox{$\\hspace{.445ex}\\notin\\hspace{.445ex}$}"},
-   {"*"           ,"\\mbox{$\\hspace{-.29ex}\\times\\hspace{-.29ex}$}"},
-   {"++"          ,"\\mbox{$\\hspace{.29ex}\\oplus\\hspace{.29ex}$}"},
-   {"--"          ,"\\mbox{$\\hspace{.29ex}\\ominus\\hspace{.29ex}$}"},
-   {"**"          ,"\\mbox{$\\hspace{.29ex}\\otimes\\hspace{.29ex}$}"},
-   {"//"          ,"\\mbox{$\\hspace{.29ex}\\oslash\\hspace{.29ex}$}"},
-   {"\\subset"    ,"\\mbox{$\\subset$}"},
-   {"\\infty"     ,"\\mbox{$\\infty$}"},
-   {"\\Box"       ,"\\mbox{$\\Box$}"},
-   {"<>"          ,"\\mbox{$\\hspace{.29ex}\\Diamond\\hspace{.29ex}$}"},
-   {" o "         ,"\\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{$\\hspace{-.083ex}\\Longrightarrow$}"},
-   {"-->"                                         ,"\\mbox{$\\longrightarrow$}"},
-   {"?!"                                          ,"\\mbox{$\\exists_1$}"},
-   {"ALL "                                        ,"\\mbox{$\\forall$}"},
-   {"EX "                                         ,"\\mbox{$\\exists$}"},
-   {"<<|"                                         ,"\\mbox{$\\ll\\!\\mid$}"},
-   {"<|"                                          ,"\\mbox{$<\\!\\mid$}"},
-   {"<=="                                         ,"\\mbox{$\\Longleftarrow$}"},
-   {"<=>"                                         ,"\\mbox{$\\Leftrightarrow$}"},
-   {"<--"                                         ,"\\mbox{$\\longleftarrow$}"},
-   {"<->"                                         ,"\\mbox{$\\leftrightarrow$}"},
-   {"and"                                         ,"\\mbox{\\bf and}"},
-   {"arities"                                     ,"\\mbox{\\bf arities}"},
-   {"axclass"                                     ,"\\mbox{\\bf axclass}"},
-   {"constdefs"                                   ,"\\mbox{\\bf constdefs}"},
-   {"consts"                                      ,"\\mbox{\\bf consts}"},
-   {"datatype"                                    ,"\\mbox{\\bf datatype}"},
-   {"defs"                                        ,"\\mbox{\\bf defs}"},
-   {"domain"                                      ,"\\mbox{\\bf domain}"},
-   {"end"                                         ,"\\mbox{\\bf end}"},
-   {"inductive"                                   ,"\\mbox{\\bf inductive}"},
-   {"instance"                                    ,"\\mbox{\\bf instance}"},
-   {"primrec"                                     ,"\\mbox{\\bf primrec}"},
-   {"recdef"                                      ,"\\mbox{\\bf recdef}"},
-   {"rules"                                       ,"\\mbox{\\bf rules}"},
-   {"syntax"                                      ,"\\mbox{\\bf syntax}"},
-   {"translations"                                ,"\\mbox{\\bf translations}"},
-   {"typedef"                                     ,"\\mbox{\\bf typedef}"},
-   {"types"                                       ,"\\mbox{\\bf types}"}
-};
-/* END_OF_SEQ_TABLE */
-
-
--- a/src/Tools/8bit/c-sources/isa2latex/conv-translate.c	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-/*
- * 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);
-  }
-}
-
--- a/src/Tools/8bit/config/Makefile	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-###############################################
-# 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'
-GMAKE= gmake
-
-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 
-
--- a/src/Tools/8bit/config/README	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-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. 
--- a/src/Tools/8bit/config/conv-tables.inp	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,432 +0,0 @@
-#   Title:      Tools/8bit/config/conf-tables.inp
-#   ID:         $Id$
-#   Author:     Franz Regensburger and David von Oheimb
-#   Copyright   1995 TU Muenchen
-############################################################
-#
-# 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
-#
-### path to the sources of the converter, 
-#   Must be readable for user.
-#   
-#   Must be delimited by "
-#
-
-CONV_SOURCE_DIR "/usr/wiss/oheimb/isabelle/src/Tools/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 
-#
->  "\#"
->  "\$"
->  "\%"
->  "\&"
->  "'"
->  "("
->  ")"
->  "{*}"
->  "+"
->  ","
->  "-"
->  "."
->  "/"
->  "0"
->  "1"
->  "2"
->  "3"
->  "4"
->  "5"
->  "6"
->  "7"
->  "8"
->  "9"
->  ":"
->  ";"
->  "<"
->  "="
->  ">"
->  "?"
->  "@"
->  "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"
->  "["
->  "\ttbackslash{}" #?????
->  "]"
->  "\^{}"			
->  "{\_\hspace{.344ex}}"
->  "`"
->  "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"
->  "\{" #"\ttlbrace{}"
->  "|"
->  "\}" #"\ttrbrace{}"
->  "\tttilde{}"
-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 "160"
-
-### 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 (i.e. double) blank space, for compensation of other too long symbols
->  "\ \ "		"  "		"\ \ "
-
-# 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"	"@"		"\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"		"\p"		"\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{$\hspace{-.33ex}\neg$}" 
->  "&\ "		"& "		"\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ " 
->  "\|\ "		"| "		"\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ " 
->  "!\ "		"!"		"\mbox{$\hspace{-.07ex}\forall$}" 
->  "\?\ "		"? "		"\mbox{$\hspace{-.07ex}\exists$}"
->  "!!"			"!!"		"\mbox{$\bigwedge$}" 
-
-# parenthesis. Pure, HOLCF, ...
->  "\\lceil"		"\lceil"	"\mbox{$\lceil$}" 
->  "\\rceil"		"\rceil"	"\mbox{$\rceil$}" 
->  "\\lfloor"		"\lfloor"	"\mbox{$\lfloor$}" 
->  "\\rfloor"		"\rfloor"	"\mbox{$\rfloor$}" 
-#> "\|-"		"|-"		"\mbox{$\vdash\hspace{-.2ex}$}"
->  "\|-"		"|-"		"\mbox{$\hspace{.49ex}\vdash\hspace{.49ex}$}"
->  "\|="		"|="		"\mbox{$\models$}"
->  "\[\|"		"[|"		"\mbox{$[\![\hspace{.32ex}$}"#\llbracket
->  "\|\]"		"|]"		"\mbox{$\hspace{.32ex}]\!]$}"#\rrbracket
->  "\\cdot"		"."		"\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}"
-
-# set theory, HOL
->  "\ :\ "		":"		"\mbox{$\hspace{.445ex}\in\hspace{.445ex}$}"
->  "\ \subseteq\ "	" <= "		"\mbox{$\subseteq$}" 
->  "\ Int\ "		" Int "		"\mbox{$\cap$}" 
->  "\ Un\ "		" Un "		"\mbox{$\cup$}" 
->  "Inter\ "		"INT "		"\mbox{$\bigcap$}"
->  "Union\ "		"UN "		"\mbox{$\bigcup$}" 
-
-# domain theory, HOLCF
->  "\\sqcap"		"\sqcap"	"\mbox{$\hspace{.29ex}\sqcap\hspace{.29ex}$}" 
->  "\\sqcup"		"\sqcup"	"\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}" 
->  "glb\ "		"glb "		"\mbox{$\overline{|\,\,|}$}"#\bigsqcap
->  "LUB\ "		"LUB "		"\mbox{$\bigsqcup$}" 
->  "UU"			"UU"		"\mbox{$\hspace{-.29ex}\bot\hspace{-.29ex}$}" 
-
-# relational symbols, Pure, HOLCF
->  "==="		".="		"\mbox{$\doteq$}" 
->  "=="			"=="		"\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}" 
->  "~="			"~="		"\mbox{$\hspace{-.34ex}\not\hspace{-.3ex}\mbox{=}$}" 
->  "\\sqsubset"		"\sqsubset"	"\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}" 
->  "<<"			"<<"		"\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}" 
->  "<:"			"<:"		"\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ " 
->  "<=:"		"<=:"		"\mbox{$\hspace{.29ex}\preceq\hspace{.29ex}$}" 
->  ":>"			":>"		"\mbox{$\hspace{.29ex}\succ\hspace{.29ex}$}\ " 
->  "~~"			"~~"		"\mbox{$\hspace{.29ex}\approx\hspace{.29ex}$}" 
->  "\\sim\ "		"\sim "		"\mbox{$\hspace{.29ex}\sim\hspace{.29ex}$}\ " 
->  "\\simeq"		"\simeq"	"\mbox{$\hspace{.29ex}\simeq\hspace{.29ex}$}" 
->  "<="			"<="		"\mbox{$\hspace{.29ex}\le\hspace{.29ex}$}" 
->  "::"			"::"		"\mbox{$:\hspace{-.07ex}:$}" #"\mbox{$\hspace{-.1ex}:\hspace{-.07ex}:\hspace{.1ex}$}" 
-
-# arrows, Pure, HOL
->  "<-"		"<-"		"\mbox{$\leftarrow$}" 
->  "-@@@@@"		"-"		"\mbox{$-$}" 
->  "->"			"->"		"\mbox{$\rightarrow$}" 
->  "\\Leftarrow"	"<="		"\mbox{$\Leftarrow$}" 
->  "=@@@@@"		"="		"\mbox{$=$}" 
->  "=>"			"=>"		"\mbox{$\hspace{.12ex}\Rightarrow$}" 
->  "\\frown"		"\frown"	"\mbox{$\frown$}" 
->  "\\mapsto"		"|->"		"\mbox{$\mapsto$}" 
->  "\\leadsto"		"~>"		"\mbox{$\hspace{.05ex}\leadsto$}" 
->  "\\uparrow"		"\uparrow"	"\mbox{$\uparrow$}" 
->  "\\downarrow"	"\downarrow"	"\mbox{$\downarrow$}" 
->  "~:"			"~:"		"\mbox{$\hspace{.445ex}\notin\hspace{.445ex}$}" 
-
-# arithmetic, HOLCF
->  "\\times"		"*"		"\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}" 
->  "\+\+"		"++"		"\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}"	#\varoplus
->  "\\ominus"		"--"		"\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}"	#\varominus
->  "\*\*"		"**"		"\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}"	#\varotimes
->  "\\oslash"		"//"		"\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" 	#\varoslash
->  "\\subset"		"\subset"	"\mbox{$\subset$}" 
->  "\\infty"		"\infty"	"\mbox{$\infty$}" 
-
-# misc
->  "\\Box"		"\Box"		"\mbox{$\Box$}" 
->  "\\Diamond"		"<>"		"\mbox{$\hspace{.29ex}\Diamond\hspace{.29ex}$}"
->  "\\circ"		" o "		"\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{$\hspace{-.083ex}\Longrightarrow$}"
-
-# HOL
->  ""		"-->"		"-->"		"\mbox{$\longrightarrow$}"
->  "!"		"\?!"		"?!"		"\mbox{$\exists_1$}"
->  "ALL@@@@@"	"ALL\ "		"ALL "		"\mbox{$\forall$}" 
->  "EX@@@@@"	"EX\ "		"EX "		"\mbox{$\exists$}" 
-
-#HOLCF
->  "<<\|"	"@<<\|"		"<<|"		"\mbox{$\ll\!\mid$}"
->  "<\|"	"@<\|"		"<|"		"\mbox{$<\!\mid$}"
-
-# misc ?
->  ""		"<=="		"<=="		"\mbox{$\Longleftarrow$}"
->  ""		"<=>"		"<=>"		"\mbox{$\Leftrightarrow$}"
->  ""		"<--"		"<--"		"\mbox{$\longleftarrow$}"
->  ""		"<->"		"<->"		"\mbox{$\leftrightarrow$}"
-#>  "\^-1"	"@\^-1"		"^-1"		"\mbox{$^{\tt -1}$}" 
-
-#Isabelle
->  "^and"	"^@and"		"and"		"\mbox{\bf and}"
->  "^arities"	"^@arities"	"arities"	"\mbox{\bf arities}"
->  "^axclass"	"^@axclass"	"axclass"	"\mbox{\bf axclass}"
->  "^constdefs"	"^@constdefs"	"constdefs"	"\mbox{\bf constdefs}"
->  "^consts"	"^@consts"	"consts"	"\mbox{\bf consts}"
->  "^datatype"	"^@datatype"	"datatype"	"\mbox{\bf datatype}"
->  "^defs"	"^@defs"	"defs"		"\mbox{\bf defs}"
->  "^domain"	"^@domain"	"domain"	"\mbox{\bf domain}"
->  "^end"	"^@end"		"end"		"\mbox{\bf end}"
->  "^inductive"	"^@inductive"	"inductive"	"\mbox{\bf inductive}"
->  "^instance"	"^@instance"	"instance"	"\mbox{\bf instance}"
->  "^primrec"	"^@primrec"	"primrec"	"\mbox{\bf primrec}"
->  "^recdef"	"^@recdef"	"recdef"	"\mbox{\bf recdef}"
->  "^rules"	"^@rules"	"rules"		"\mbox{\bf rules}"
->  "^syntax"	"^@syntax"	"syntax"	"\mbox{\bf syntax}"
->  "^translations""^@translations""translations""\mbox{\bf translations}"
->  "^typedef"	"^@typedef"	"typedef"	"\mbox{\bf typedef}"
->  "^types"	"^@types"	"types"		"\mbox{\bf types}"
-END_SEQ_TABLE
-
-
--- a/src/Tools/8bit/config/key-table.inp	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,188 +0,0 @@
-############################################################
-# 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 space	CODE a0
-	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 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 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 Mod4	KEY x		CODE f2
-	MOD None	KEY F2		CODE e4
-	MOD None	KEY F3		CODE dd
-	MOD None	KEY F4		CODE cf
-	MOD None	KEY F5		CODE ce
-	MOD None	KEY F6		CODE f1
-	MOD None	KEY F7		CODE e5
-	MOD None	KEY F8		CODE da
-	MOD None	KEY F9		CODE c4
-	MOD None	KEY F10		CODE cb
-	MOD None	KEY F11		CODE cc
-	MOD None	KEY F12		CODE ea,eb
-	MOD Shift	KEY F1		CODE e9
-	MOD Shift	KEY F2		CODE ea
-	MOD Shift	KEY F3		CODE eb
-	MOD Shift	KEY F4		CODE e9,eb
-	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 ca
-	MOD Shift	KEY F10		CODE c9
-	MOD Ctrl	KEY F1		CODE e6
-	MOD Ctrl	KEY F2		CODE e7
-	MOD Ctrl	KEY F3		CODE e8
-	MOD Ctrl	KEY F4		CODE e6,e8
-	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 fd
-	MOD Ctrl	KEY F10		CODE cd
-	MOD Mod2	KEY F1		CODE ed
-	MOD Mod2	KEY F2		CODE ee
-	MOD Mod2	KEY F3		CODE ef
-	MOD Mod2	KEY F4		CODE f0
-	MOD Mod2	KEY F5		CODE d4
-	MOD Mod2	KEY F6		CODE d5
-	MOD Mod2	KEY F7		CODE d6
-	MOD Mod2	KEY F8		CODE d7
-	MOD Mod2	KEY F9		CODE dc
-	MOD Mod2	KEY F10		CODE f8
-	MOD Mod4	KEY F1		CODE f9
-	MOD Mod4	KEY F2		CODE fa
-	MOD Mod4	KEY F3		CODE fb
-	MOD Mod4	KEY F4		CODE fc
-	MOD Mod4	KEY F5		CODE d0
-	MOD Mod4	KEY F6		CODE d1
-	MOD Mod4	KEY F7		CODE d2
-	MOD Mod4	KEY F8		CODE d3
-	MOD Mod4	KEY F9		CODE f7
-	MOD Mod4	KEY F10		CODE ec
-	MOD Mod4	KEY F11		CODE fe
-	MOD Mod4	KEY F12		CODE ff
-END_KEY_MAP
-
-
--- a/src/Tools/8bit/doc/Makefile	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-###############################################
-# 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=latex2e
-ISA2LATEX=../bin/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
-
-all: manual.dvi fontdocfiles
-
-fontdocfiles: $(FONTDOCFILES)
-
-manual.dvi: manual.tex
-	$(LATEX) $< >/dev/null; $(LATEX) $<
-clean:
-	rm -f *.tex *.aux *.log
--- a/src/Tools/8bit/doc/Set2.thy	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-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"
-
--- a/src/Tools/8bit/doc/Set2_a.thy	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-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"
-
--- a/src/Tools/8bit/doc/Set2_g.thy	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-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"
-
--- a/src/Tools/8bit/doc/Set2g.thy	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-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"
-
--- a/src/Tools/8bit/doc/Set2x.thy	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-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"
-
--- a/src/Tools/8bit/doc/manual.itex	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,448 +0,0 @@
-\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, and alternatively a \LaTeX{} 
-command format, is provided. There are editors and a terminal
-capable of inputting and displaying the graphical characters, and converters
-between the different representations. The graphical font extends the normal
-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.
-
-\pagebreak
-
-\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.
-
-
-\pagebreak
-
-\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}
-
-\pagebreak
-
-\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
-
-
-\pagebreak
-
-\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, for example,
-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@'.
-
-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}.
-
-\pagebreak
-
-\section{Technical issues}
-
-\subsection{Preparations}
-
-To use the 8bit package, you have to set (respectively extend) the content of
-the following environment variables and export them:
-
-\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}.
-Configure the \bt{Makefile} there, then run \bt{gmake clean} 
-(\bt{gmake} is the gnu version of \bt{make}) and then \bt{gmake}.
-
-If you want to adapt the configuration of the font (keyboard bindings or
-conversion tables used by \bt{isa2latex}), change directory to\\
-\bt{\$ISABELLE8BIT/config} ,
-edit the files \bt{key-table.inp} and \bt{conv-tables.inp} 
-as described below, 
-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.
-
-%%%% FRANZ
-\subsubsection{Configuring conversion tables and keyboard bindings}
-%\label{subsub:gens}
-
-The 8bit package comes along with several perl%
-\footnote{the scripts are written in perl4. In order to run them with later
-  versions of perl, you have to patch the scripts in some places since perl4
-  and later versions differ in the way they expand backslashes.} scripts that
-allow you to configure the package for your own needs in a convenient way.
-
-Keyboard bindings and the major behaviour of the converter \bt{isa2latex} are
-controlled by the two configuration files \bt{key-table.inp} and
-\bt{conv-tables.inp} which reside in the directory \bt{\$ISABELLE8BIT/config}.
-As these files contain a lot of comments, their formats are rather 
-self explanatory.
-
-To change the conversions performed by \bt{isa2latex}, you just
-have to alter the file \bt{conv-tables.inp}. This file mainly contains the
-conversion tables for single characters in the code ranges 32 -- 127 and
-(usually) 161 -- 255.  The last part of the configuration file describes how the
-lexical analyser of the converter \bt{isa2latex} treats special character
-sequences. It is most likely that you change this part of the configuration
-file. 
-In order to activate your changes, you have to run the Makefile with \bt{gmake}.
-This invokes the perl script \bt{gen-isa2latex} with \bt{conv-tables.inp} as
-an argument. See the man page on \bt{gen-isa2latex} for more details about
-command line arguments. According to the configuration file, the perl script
-patches specific portions of the C source of the 
-converter in the directory \bt{\$ISABELLE8BIT/c-sources/isa2latex} and
-calls the C compiler to generate a new binary for \bt{isa2latex}\footnote{
-The \bt{Makefile} uses the lexical analyzer \bt{flex}. Make sure that you
-use a recent version of it.}.
-
-If you want to alter the keyboard bindings for the various editors and the
-terminal, you have to change the configuration file \bt{key-table.inp}. 
-The file contains as its main part a table relating keystrokes to the 
-keyboard codes to be generated. Then run the Makefile with \bt{gmake}.
-For every editor that the 8bit package supports, \bt{gmake} starts a perl script
-that patches the start up file for the specific editor. For example, for the 
-\bt{vim} editor the script \bt{gen-isavim} is started, which patches the shell 
-script
-\bt{\$ISABELLE8BIT/vim/isavim}.  As the last action, the perl script
-\bt{gen-isadoc} is invoked which generates some \bt{.dvi} files for reference
-cards which document the new keyboard mapping.
-%%%% FRANZ
-
-\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}.
-You can call the \bt{patcher} than 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}
-
-
--- a/src/Tools/8bit/doc/palette.isa	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-          
-
-           
-
-       
-        
-     ''     
- 
-        
-        
-
-          
-     
-
-           
-         
-
-        
--- a/src/Tools/8bit/fonts/bash.inputrc	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-set meta-flag On
-set convert-meta Off
-set output-meta On
--- a/src/Tools/8bit/fonts/bdf-code.txt	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-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
--- a/src/Tools/8bit/fonts/fonts.dir	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-6
-spcr14.bdf spcr14
-isacr14.bdf isacr14
-isacb24.bdf isacb24
-oldisacr14.bdf oldisacr14
-isabelle14.bdf isabelle14
-isabelle24.bdf isabelle24
--- a/src/Tools/8bit/fonts/install	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-#!/bin/bash
-
-#NOTE: just a quick and dirty hack -- assumes correct isatool in PATH
-
-isatool installfonts
--- a/src/Tools/8bit/fonts/isabelle14.bdf	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2944 +0,0 @@
-STARTFONT 2.1
-FONT -isabelle-fixed-medium-r-normal--14-140-75-75-m-90-isabelle-0
-SIZE 14 75 75
-FONTBOUNDINGBOX 9 14 4 -3
-STARTPROPERTIES 22
-FONTNAME_REGISTRY ""
-FOUNDRY "Isabelle"
-FAMILY_NAME "Fixed"
-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 "Isabelle"
-CHARSET_ENCODING "0"
-CHARSET_COLLECTIONS ""
-FULL_NAME "Fixed"
-COPYRIGHT "Public"
-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
-70
-88
-80
-40
-30
-08
-88
-70
-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 4 10 1 0
-BITMAP
-20
-60
-a0
-20
-20
-20
-20
-20
-20
-70
-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
-80
-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
-08
-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 6 10 1 -1
-BITMAP
-38
-44
-84
-9c
-a4
-a4
-9c
-80
-40
-38
-ENDCHAR
-STARTCHAR A
-ENCODING 65
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-10
-10
-28
-28
-44
-7c
-82
-82
-82
-ENDCHAR
-STARTCHAR B
-ENCODING 66
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-f8
-84
-84
-84
-f8
-84
-84
-84
-f8
-ENDCHAR
-STARTCHAR C
-ENCODING 67
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-3c
-42
-80
-80
-80
-80
-80
-42
-3c
-ENDCHAR
-STARTCHAR D
-ENCODING 68
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-f8
-84
-82
-82
-82
-82
-82
-84
-f8
-ENDCHAR
-STARTCHAR E
-ENCODING 69
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-fc
-80
-80
-80
-f0
-80
-80
-80
-fc
-ENDCHAR
-STARTCHAR F
-ENCODING 70
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-fc
-80
-80
-80
-f0
-80
-80
-80
-80
-ENDCHAR
-STARTCHAR G
-ENCODING 71
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 0 0
-BITMAP
-3c
-42
-80
-80
-80
-8e
-82
-42
-3c
-ENDCHAR
-STARTCHAR H
-ENCODING 72
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-84
-84
-84
-84
-fc
-84
-84
-84
-84
-ENDCHAR
-STARTCHAR I
-ENCODING 73
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 3 9 2 0
-BITMAP
-e0
-40
-40
-40
-40
-40
-40
-40
-e0
-ENDCHAR
-STARTCHAR J
-ENCODING 74
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-1c
-08
-08
-08
-08
-88
-88
-88
-70
-ENDCHAR
-STARTCHAR K
-ENCODING 75
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-84
-88
-90
-a0
-e0
-90
-88
-88
-84
-ENDCHAR
-STARTCHAR L
-ENCODING 76
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 0 0
-BITMAP
-e0
-40
-40
-40
-40
-40
-40
-42
-7e
-ENDCHAR
-STARTCHAR M
-ENCODING 77
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-c6
-c6
-aa
-aa
-92
-92
-82
-82
-82
-ENDCHAR
-STARTCHAR N
-ENCODING 78
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-c4
-c4
-a4
-a4
-94
-94
-8c
-8c
-84
-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 6 9 1 0
-BITMAP
-f8
-84
-84
-84
-84
-f8
-80
-80
-80
-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 7 9 1 0
-BITMAP
-f8
-84
-84
-84
-88
-f0
-88
-84
-82
-ENDCHAR
-STARTCHAR S
-ENCODING 83
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-78
-84
-80
-80
-78
-04
-04
-84
-78
-ENDCHAR
-STARTCHAR T
-ENCODING 84
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-fe
-10
-10
-10
-10
-10
-10
-10
-10
-ENDCHAR
-STARTCHAR U
-ENCODING 85
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-84
-84
-84
-84
-84
-84
-84
-84
-78
-ENDCHAR
-STARTCHAR V
-ENCODING 86
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-82
-82
-82
-44
-44
-28
-28
-10
-10
-ENDCHAR
-STARTCHAR W
-ENCODING 87
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-82
-82
-92
-92
-aa
-aa
-44
-44
-44
-ENDCHAR
-STARTCHAR X
-ENCODING 88
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 9 0 0
-BITMAP
-81
-42
-24
-24
-18
-24
-24
-42
-81
-ENDCHAR
-STARTCHAR Y
-ENCODING 89
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 9 1 0
-BITMAP
-82
-44
-44
-28
-28
-10
-10
-10
-10
-ENDCHAR
-STARTCHAR Z
-ENCODING 90
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-fc
-04
-08
-10
-20
-20
-40
-80
-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
-04
-04
-7c
-84
-8c
-76
-ENDCHAR
-STARTCHAR b
-ENCODING 98
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 10 1 0
-BITMAP
-80
-80
-80
-b8
-c4
-82
-82
-82
-c4
-b8
-ENDCHAR
-STARTCHAR c
-ENCODING 99
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 7 1 0
-BITMAP
-3c
-42
-80
-80
-80
-42
-3c
-ENDCHAR
-STARTCHAR d
-ENCODING 100
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 10 0 0
-BITMAP
-02
-02
-02
-3a
-46
-82
-82
-82
-46
-3a
-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
-20
-ENDCHAR
-STARTCHAR g
-ENCODING 103
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 10 0 -3
-BITMAP
-3a
-46
-82
-82
-82
-46
-3a
-02
-04
-78
-ENDCHAR
-STARTCHAR h
-ENCODING 104
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 10 1 0
-BITMAP
-80
-80
-80
-b8
-c4
-84
-84
-84
-84
-84
-ENDCHAR
-STARTCHAR i
-ENCODING 105
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 3 10 3 0
-BITMAP
-40
-40
-00
-c0
-40
-40
-40
-40
-40
-e0
-ENDCHAR
-STARTCHAR j
-ENCODING 106
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 4 13 1 -3
-BITMAP
-10
-10
-00
-30
-10
-10
-10
-10
-10
-10
-10
-20
-c0
-ENDCHAR
-STARTCHAR k
-ENCODING 107
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 5 9 1 0
-BITMAP
-80
-80
-98
-90
-a0
-c0
-a0
-90
-98
-ENDCHAR
-STARTCHAR l
-ENCODING 108
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 3 9 3 0
-BITMAP
-c0
-40
-40
-40
-40
-40
-40
-40
-e0
-ENDCHAR
-STARTCHAR m
-ENCODING 109
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 7 0 0
-BITMAP
-db
-6d
-49
-49
-49
-49
-49
-ENDCHAR
-STARTCHAR n
-ENCODING 110
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 7 0 0
-BITMAP
-dc
-62
-42
-42
-42
-42
-42
-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 7 10 1 -3
-BITMAP
-b8
-c4
-82
-82
-82
-c4
-b8
-80
-80
-80
-ENDCHAR
-STARTCHAR q
-ENCODING 113
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 10 0 -3
-BITMAP
-3a
-46
-82
-82
-82
-46
-3a
-02
-02
-02
-ENDCHAR
-STARTCHAR r
-ENCODING 114
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-98
-a4
-c0
-80
-80
-80
-80
-ENDCHAR
-STARTCHAR s
-ENCODING 115
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-78
-84
-80
-78
-04
-84
-78
-ENDCHAR
-STARTCHAR t
-ENCODING 116
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 9 1 0
-BITMAP
-40
-40
-f0
-40
-40
-40
-40
-44
-38
-ENDCHAR
-STARTCHAR u
-ENCODING 117
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 7 1 0
-BITMAP
-84
-84
-84
-84
-84
-8c
-76
-ENDCHAR
-STARTCHAR v
-ENCODING 118
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-84
-84
-84
-48
-48
-30
-30
-ENDCHAR
-STARTCHAR w
-ENCODING 119
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 7 1 0
-BITMAP
-82
-82
-92
-92
-54
-6c
-6c
-ENDCHAR
-STARTCHAR x
-ENCODING 120
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 7 1 0
-BITMAP
-c6
-44
-28
-10
-28
-44
-c6
-ENDCHAR
-STARTCHAR y
-ENCODING 121
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 10 1 -3
-BITMAP
-84
-84
-84
-48
-48
-30
-10
-20
-20
-60
-ENDCHAR
-STARTCHAR z
-ENCODING 122
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 5 7 1 0
-BITMAP
-f8
-08
-10
-20
-40
-80
-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 10 1 -1
-BITMAP
-fe
-62
-60
-60
-60
-60
-60
-60
-60
-f0
-ENDCHAR
-STARTCHAR Delta
-ENCODING 162
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 9 10 0 -1
-BITMAP
-0800
-0800
-1c00
-1c00
-1600
-2600
-2300
-4300
-4180
-ff80
-ENDCHAR
-STARTCHAR Theta
-ENCODING 163
-SWIDTH 264 0
-DWIDTH 9 0
-BBX 9 10 1 -1
-BITMAP
-3e00
-4100
-c180
-c180
-dd80
-dd80
-c180
-c180
-4100
-3e00
-ENDCHAR
-STARTCHAR Lambda
-ENCODING 164
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 9 10 0 -1
-BITMAP
-0800
-0800
-1c00
-1c00
-1600
-2600
-2300
-4300
-4180
-e380
-ENDCHAR
-STARTCHAR Pi
-ENCODING 165
-SWIDTH 264 0
-DWIDTH 9 0
-BBX 9 10 0 -1
-BITMAP
-ff80
-6300
-6300
-6300
-6300
-6300
-6300
-6300
-6300
-f780
-ENDCHAR
-STARTCHAR Sigma
-ENCODING 166
-SWIDTH 240 0
-DWIDTH 9 0
-BBX 9 10 1 -1
-BITMAP
-7f80
-3080
-1800
-0c00
-0400
-0800
-1000
-3080
-7f80
-ff00
-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
-30
-18
-08
-08
-18
-18
-34
-64
-62
-c3
-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 phi
-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 6 4 1 0
-BITMAP
-fc
-04
-04
-04
-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 And
-ENCODING 196
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 7 12 1 -2
-BITMAP
-10
-10
-10
-28
-28
-28
-44
-44
-44
-82
-82
-82
-ENDCHAR
-STARTCHAR lceil
-ENCODING 197
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 5 12 1 -2
-BITMAP
-f8
-80
-80
-80
-80
-80
-80
-80
-80
-80
-80
-80
-ENDCHAR
-STARTCHAR rceil
-ENCODING 198
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 5 12 1 -2
-BITMAP
-f8
-08
-08
-08
-08
-08
-08
-08
-08
-08
-08
-08
-ENDCHAR
-STARTCHAR lfloor
-ENCODING 199
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 5 12 1 -2
-BITMAP
-80
-80
-80
-80
-80
-80
-80
-80
-80
-80
-80
-f8
-ENDCHAR
-STARTCHAR rfloor
-ENCODING 200
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 5 12 1 -2
-BITMAP
-08
-08
-08
-08
-08
-08
-08
-08
-08
-08
-08
-f8
-ENDCHAR
-STARTCHAR turnstile
-ENCODING 201
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 9 3 0
-BITMAP
-80
-80
-80
-80
-ff
-80
-80
-80
-80
-ENDCHAR
-STARTCHAR Turnstile
-ENCODING 202
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 9 3 0
-BITMAP
-80
-80
-80
-ff
-80
-ff
-80
-80
-80
-ENDCHAR
-STARTCHAR lbrakk
-ENCODING 203
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 12 1 -2
-BITMAP
-fc
-a0
-a0
-a0
-a0
-a0
-a0
-a0
-a0
-a0
-a0
-fc
-ENDCHAR
-STARTCHAR rbrakk
-ENCODING 204
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 6 12 1 -2
-BITMAP
-fc
-14
-14
-14
-14
-14
-14
-14
-14
-14
-14
-fc
-ENDCHAR
-STARTCHAR cdot
-ENCODING 205
-SWIDTH 600 0
-DWIDTH 8 0
-BBX 2 2 3 3
-BITMAP
-c0
-c0
-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 -3
-BITMAP
-7c
-80
-80
-80
-7c
-00
-fc
-00
-00
-00
-ENDCHAR
-STARTCHAR inter
-ENCODING 208
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-78
-84
-84
-84
-84
-84
-84
-ENDCHAR
-STARTCHAR union
-ENCODING 209
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-84
-84
-84
-84
-84
-84
-78
-ENDCHAR
-STARTCHAR Inter
-ENCODING 210
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 10 1 -1
-BITMAP
-3c
-42
-81
-81
-81
-81
-81
-81
-81
-81
-ENDCHAR
-STARTCHAR Union
-ENCODING 211
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 10 1 -1
-BITMAP
-81
-81
-81
-81
-81
-81
-81
-81
-42
-3c
-ENDCHAR
-STARTCHAR sqinter
-ENCODING 212
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-fc
-84
-84
-84
-84
-84
-84
-ENDCHAR
-STARTCHAR squnion
-ENCODING 213
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 6 7 1 0
-BITMAP
-84
-84
-84
-84
-84
-84
-fc
-ENDCHAR
-STARTCHAR Sqinter
-ENCODING 214
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 10 1 -1
-BITMAP
-ff
-81
-81
-81
-81
-81
-81
-81
-81
-81
-ENDCHAR
-STARTCHAR Squnion
-ENCODING 215
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 10 1 -1
-BITMAP
-81
-81
-81
-81
-81
-81
-81
-81
-81
-ff
-ENDCHAR
-STARTCHAR bottom
-ENCODING 216
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 7 8 1 0
-BITMAP
-10
-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 noteq
-ENCODING 219
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 7 7 1 0
-BITMAP
-08
-08
-fe
-10
-fe
-20
-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 7 1 0
-BITMAP
-fc
-80
-80
-80
-fc
-00
-fc
-ENDCHAR
-STARTCHAR prec
-ENCODING 222
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 7 7 1 1
-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 1
-BITMAP
-80
-40
-30
-0e
-30
-40
-80
-ENDCHAR
-STARTCHAR approx
-ENCODING 225
-SWIDTH 240 0
-DWIDTH 9 0
-BBX 7 6 1 1
-BITMAP
-60
-92
-0c
-60
-92
-0c
-ENDCHAR
-STARTCHAR sim
-ENCODING 226
-SWIDTH 240 0
-DWIDTH 9 0
-BBX 7 3 1 2
-BITMAP
-60
-92
-0c
-ENDCHAR
-STARTCHAR simeq
-ENCODING 227
-SWIDTH 240 0
-DWIDTH 9 0
-BBX 7 5 1 1
-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 Colon
-ENCODING 229
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 4 7 2 0
-BITMAP
-90
-90
-00
-00
-00
-90
-90
-ENDCHAR
-STARTCHAR leftarrow
-ENCODING 230
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 9 5 0 2
-BITMAP
-3000
-6000
-ff80
-6000
-3000
-ENDCHAR
-STARTCHAR midarrow
-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 9 5 0 2
-BITMAP
-0600
-0300
-ff80
-0300
-0600
-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 Midarrow
-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 9 7 0 0
-BITMAP
-0c00
-0600
-ff00
-0180
-ff00
-0600
-0c00
-ENDCHAR
-STARTCHAR bow
-ENCODING 236
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 8 3 0 4
-BITMAP
-3c
-42
-81
-ENDCHAR
-STARTCHAR mapsto
-ENCODING 237
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 8 5 1 2
-BITMAP
-84
-82
-ff
-82
-84
-ENDCHAR
-STARTCHAR leadsto
-ENCODING 238
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 8 5 0 2
-BITMAP
-04
-62
-93
-0e
-04
-ENDCHAR
-STARTCHAR up
-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 down
-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 notin
-ENCODING 241
-SWIDTH 216 0
-DWIDTH 9 0
-BBX 6 11 1 -3
-BITMAP
-08
-3c
-48
-90
-f8
-90
-60
-3c
-20
-00
-00
-ENDCHAR
-STARTCHAR times
-ENCODING 242
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 6 6 1 1
-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 subset
-ENCODING 247
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 6 10 1 -3
-BITMAP
-7c
-80
-80
-80
-7c
-00
-00
-00
-00
-00
-ENDCHAR
-STARTCHAR infinity
-ENCODING 248
-SWIDTH 666 0
-DWIDTH 9 0
-BBX 9 5 1 2
-BITMAP
-7700
-8c80
-8880
-9880
-7700
-ENDCHAR
-STARTCHAR box
-ENCODING 249
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 8 8 1 0
-BITMAP
-ff
-81
-81
-81
-81
-81
-81
-ff
-ENDCHAR
-STARTCHAR diamond
-ENCODING 250
-SWIDTH 600 0
-DWIDTH 9 0
-BBX 9 9 1 0
-BITMAP
-0800
-1400
-2200
-4100
-8080
-4100
-2200
-1400
-0800
-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
--- a/src/Tools/8bit/fonts/isabelle24.bdf	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3810 +0,0 @@
-STARTFONT 2.1
-FONT -isabelle-fixed-bold-r-normal--24-240-75-75-m-150-isabelle-0
-SIZE 24 75 75
-FONTBOUNDINGBOX 16 22 6 -5
-STARTPROPERTIES 22
-FONTNAME_REGISTRY ""
-FOUNDRY "Isabelle"
-FAMILY_NAME "Fixed"
-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 "Isabelle"
-CHARSET_ENCODING "0"
-CHARSET_COLLECTIONS ""
-FULL_NAME "Fixed Bold"
-COPYRIGHT "Public"
-FONT_ASCENT 17
-FONT_DESCENT 5
-CAP_HEIGHT 15
-X_HEIGHT 11
-ENDPROPERTIES
-CHARS 191
-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 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 15 1 0
-BITMAP
-ffc0
-7040
-7000
-7000
-7000
-7000
-7000
-7000
-7000
-7000
-7000
-7000
-7000
-7000
-f800
-ENDCHAR
-STARTCHAR Delta
-ENCODING 162
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 11 15 1 0
-BITMAP
-0600
-0600
-0e00
-0f00
-1f00
-1b00
-1380
-3180
-3180
-21c0
-60c0
-60c0
-c0e0
-c060
-ffe0
-ENDCHAR
-STARTCHAR Theta
-ENCODING 163
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 12 15 1 0
-BITMAP
-1f80
-3fc0
-6060
-c030
-c030
-d0b0
-dfb0
-dfb0
-d0b0
-c030
-c030
-c030
-6060
-3fc0
-1f80
-ENDCHAR
-STARTCHAR Lambda
-ENCODING 164
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 12 15 1 0
-BITMAP
-0600
-0600
-0e00
-0f00
-1f00
-1b00
-1380
-3180
-3180
-21c0
-60c0
-60c0
-c0e0
-c060
-e0f0
-ENDCHAR
-STARTCHAR C167
-ENCODING 165
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 13 15 1 0
-BITMAP
-fff8
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-3060
-78f0
-ENDCHAR
-STARTCHAR C167
-ENCODING 166
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 13 15 1 0
-BITMAP
-fff8
-e008
-7000
-3800
-1c00
-0e00
-0700
-0300
-0600
-0c00
-1800
-3008
-7ff8
-fff0
-ffe0
-ENDCHAR
-STARTCHAR C167
-ENCODING 167
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 12 14 1 0
-BITMAP
-0f00
-0600
-0600
-1f80
-76e0
-6660
-c630
-8610
-c630
-6660
-76e0
-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 8 6 2 1
-BITMAP
-ff
-ff
-03
-03
-03
-03
-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 9 14 1 0
-BITMAP
-ff80
-ff80
-0180
-0180
-0180
-0180
-ff80
-ff80
-0180
-0180
-0180
-0180
-ff80
-ff80
-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 8 15 1 -1
-BITMAP
-ff
-ff
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-ENDCHAR
-STARTCHAR C197
-ENCODING 198
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 15 1 -1
-BITMAP
-ff
-ff
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-ENDCHAR
-STARTCHAR C197
-ENCODING 199
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 15 1 -1
-BITMAP
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-c0
-ff
-ff
-ENDCHAR
-STARTCHAR C197
-ENCODING 200
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 15 1 -1
-BITMAP
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-03
-ff
-ff
-ENDCHAR
-STARTCHAR turnstile
-ENCODING 201
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 11 14 1 0
-BITMAP
-c000
-c000
-c000
-c000
-c000
-c000
-ffe0
-ffe0
-c000
-c000
-c000
-c000
-c000
-c000
-ENDCHAR
-STARTCHAR Turnstile
-ENCODING 202
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 11 14 1 0
-BITMAP
-c000
-c000
-c000
-c000
-ffe0
-ffe0
-c000
-c000
-ffe0
-ffe0
-c000
-c000
-c000
-c000
-ENDCHAR
-STARTCHAR C203
-ENCODING 203
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 14 1 0
-BITMAP
-ff
-ff
-d8
-d8
-d8
-d8
-d8
-d8
-d8
-d8
-d8
-d8
-ff
-ff
-ENDCHAR
-STARTCHAR C204
-ENCODING 204
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 14 1 0
-BITMAP
-ff
-ff
-1b
-1b
-1b
-1b
-1b
-1b
-1b
-1b
-1b
-1b
-ff
-ff
-ENDCHAR
-STARTCHAR cdot
-ENCODING 205
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 3 3 1 4
-BITMAP
-e0
-e0
-e0
-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 12 1 0
-BITMAP
-0600
-0600
-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 3
-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 2
-BITMAP
-ff80
-ff80
-0000
-ff80
-ff80
-0000
-ff80
-ff80
-ENDCHAR
-STARTCHAR C161
-ENCODING 219
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 10 12 1 0
-BITMAP
-0600
-0600
-0600
-ffc0
-ffc0
-0c00
-0c00
-ffc0
-ffc0
-1800
-1800
-1800
-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 C161
-ENCODING 225
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 12 8 1 3
-BITMAP
-3800
-fe30
-c7f0
-01c0
-3800
-fe30
-c7f0
-01c0
-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 7 10 1 1
-BITMAP
-c6
-c6
-00
-00
-00
-00
-00
-00
-c6
-c6
-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 11 4 1 7
-BITMAP
-3f80
-7fc0
-e0e0
-c060
-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 C161
-ENCODING 247
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 11 8 1 3
-BITMAP
-1fe0
-7fe0
-e000
-c000
-c000
-e000
-7fe0
-1fe0
-ENDCHAR
-STARTCHAR C161
-ENCODING 248
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 14 8 0 2
-BITMAP
-3870
-7cf8
-e7dc
-c38c
-c70c
-ef9c
-7cf8
-3870
-ENDCHAR
-STARTCHAR C161
-ENCODING 249
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 12 12 1 0
-BITMAP
-fff0
-fff0
-c030
-c030
-c030
-c030
-c030
-c030
-c030
-c030
-fff0
-fff0
-ENDCHAR
-STARTCHAR C161
-ENCODING 250
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 13 13 1 0
-BITMAP
-0200
-0700
-0d80
-18c0
-3060
-6030
-c018
-6030
-3060
-18c0
-0d80
-0700
-0200
-ENDCHAR
-STARTCHAR C161
-ENCODING 251
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 8 1 2
-BITMAP
-3c
-7e
-e7
-c3
-c3
-e7
-7e
-3c
-ENDCHAR
-STARTCHAR C161
-ENCODING 252
-SWIDTH 600 0
-DWIDTH 15 0
-BBX 8 8 1 2
-BITMAP
-3c
-7e
-ff
-ff
-ff
-ff
-7e
-3c
-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
--- a/src/Tools/8bit/fonts/isacb24.bdf	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3936 +0,0 @@
-STARTFONT 2.1
-FONT isacb24
-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 ""
-FULL_NAME "Isabelle24 Bold"
-COPYRIGHT "Copyright (c)1985,1987 Adobe Systems, Inc., Portions Copyright 1988, Portions Copyright 1995 TU Muenchen"
-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