# HG changeset patch
# User oheimb
# Date 850498327 -3600
# Node ID 2fb9659d30ca3779b2632ee681a90abc9e77a8db
# Parent  de76cee7a30c817ce88dda08ab6baaca5e18f2e8
minor adaptions

diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/Makefile
--- a/src/Tools/8bit/Makefile	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/Makefile	Fri Dec 13 18:32:07 1996 +0100
@@ -55,7 +55,7 @@
 CONFIGFILES = config/Makefile config/key-table.inp config/conv-tables.inp
 
 #path stem to isabelle source, used by patcher
-STEM = /usr/stud/oheimb/isabelle/
+STEM = /usr/wiss/oheimb/isabelle/
 
 ###############################################
 # configuration for configuration files in ./config
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/c-sources/a2isa/a2isa
Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/c-sources/isa2latex/isa2latex
Binary file src/Tools/8bit/c-sources/isa2latex/isa2latex has changed
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/doc/Makefile
--- a/src/Tools/8bit/doc/Makefile	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/doc/Makefile	Fri Dec 13 18:32:07 1996 +0100
@@ -28,9 +28,7 @@
 
 fontdocfiles: $(FONTDOCFILES)
 
-manual: manual.tex manual.dvi
-
-manual.tex: manual.itex
+manual: manual.dvi
 
 clean:
 	rm -f *.aux *.log
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/doc/manual.dvi
Binary file src/Tools/8bit/doc/manual.dvi has changed
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/doc/manual.itex
--- a/src/Tools/8bit/doc/manual.itex	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/doc/manual.itex	Fri Dec 13 18:32:07 1996 +0100
@@ -413,7 +413,9 @@
 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}.
+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}. 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/fonts/isacb24.bdf
--- a/src/Tools/8bit/fonts/isacb24.bdf	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/fonts/isacb24.bdf	Fri Dec 13 18:32:07 1996 +0100
@@ -1,5 +1,5 @@
 STARTFONT 2.1
-FONT spcb24
+FONT isacb24
 SIZE 24 75 75
 FONTBOUNDINGBOX 16 22 6 -5
 STARTPROPERTIES 22
@@ -18,9 +18,9 @@
 AVERAGE_WIDTH 150
 CHARSET_REGISTRY "ISO8859"
 CHARSET_ENCODING "1"
-CHARSET_COLLECTIONS "ASCII ISO8859-1 ADOBE-STANDARD"
-FULL_NAME "Courier Bold"
-COPYRIGHT "Copyright (c)1985,1987 Adobe Systems, Inc., Portions Copyright 1988"
+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
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/fonts/isacr14.bdf
--- a/src/Tools/8bit/fonts/isacr14.bdf	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/fonts/isacr14.bdf	Fri Dec 13 18:32:07 1996 +0100
@@ -33,8 +33,8 @@
 FONTBOUNDINGBOX 9 14 4 -3
 STARTPROPERTIES 22
 FONTNAME_REGISTRY ""
-FAMILY_NAME "Isabelle"
-FOUNDRY ""
+FAMILY_NAME "Courier"
+FOUNDRY "Adobe"
 WEIGHT_NAME "Medium"
 SLANT "R"
 SETWIDTH_NAME "Normal"
@@ -45,11 +45,11 @@
 RESOLUTION_Y 75
 SPACING "M"
 AVERAGE_WIDTH 90
-CHARSET_REGISTRY ""
+CHARSET_REGISTRY "ISO8859"
 CHARSET_ENCODING "1"
 CHARSET_COLLECTIONS ""
 FULL_NAME "Isabelle14"
-COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1993 TU Muenchen"
+COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1995 TU Muenchen"
 FONT_ASCENT 11
 FONT_DESCENT 3
 CAP_HEIGHT 9
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOL/add-HOL.cfg
--- a/src/Tools/8bit/isa-patches/HOL/add-HOL.cfg	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOL/add-HOL.cfg	Fri Dec 13 18:32:07 1996 +0100
@@ -1,6 +1,6 @@
 Configuration file for adding the 8bit patches to Isabelle
 
-STEM "/usr/stud/oheimb/isabelle/"
+STEM "/usr/wiss/oheimb/isabelle/"
 
 ADD Tools/8bit/isa-patches/HOL/HOL1.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
 ADD Tools/8bit/isa-patches/HOL/HOL2.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg
--- a/src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg	Fri Dec 13 18:32:07 1996 +0100
@@ -1,6 +1,6 @@
 Configuration file for cleaning the 8bit patches in Isabelle
 
-STEM "/usr/stud/oheimb/isabelle/"
+STEM "/usr/wiss/oheimb/isabelle/"
 
 CLEAN IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
 CLEAN IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg
--- a/src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg	Fri Dec 13 18:32:07 1996 +0100
@@ -1,6 +1,6 @@
 Configuration file for extracting the 8bit patches from Isabelle
 
-STEM "/usr/stud/oheimb/isabelle/"
+STEM "/usr/wiss/oheimb/isabelle/"
 
 EXTRACT Tools/8bit/isa-patches/HOL/HOL1.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
 EXTRACT Tools/8bit/isa-patches/HOL/HOL2.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOLCF/Up3.p
--- a/src/Tools/8bit/isa-patches/HOLCF/Up3.p	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/Up3.p	Fri Dec 13 18:32:07 1996 +0100
@@ -1,3 +1,3 @@
 translations
-"case l of up`x => t1" == "lift`(¤x.t1)`l"
+"case l of up`x => t1" == "fup`(¤x.t1)`l"
 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg
--- a/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg	Fri Dec 13 18:32:07 1996 +0100
@@ -1,6 +1,6 @@
 Configuration file for adding the 8bit patches to Isabelle
 
-STEM "/usr/stud/oheimb/isabelle/"
+STEM "/usr/wiss/oheimb/isabelle/"
 
 ADD Tools/8bit/isa-patches/HOLCF/Cfun1.p IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
 ADD Tools/8bit/isa-patches/HOLCF/Cfun1.p2 IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
--- a/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg	Fri Dec 13 18:32:07 1996 +0100
@@ -1,6 +1,6 @@
 Configuration file for cleaning the 8bit patches in Isabelle
 
-STEM "/usr/stud/oheimb/isabelle/"
+STEM "/usr/wiss/oheimb/isabelle/"
 
 CLEAN IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
 CLEAN IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg
--- a/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg	Fri Dec 13 18:32:07 1996 +0100
@@ -1,6 +1,6 @@
 Configuration file for extracting the 8bit patches from Isabelle
 
-STEM "/usr/stud/oheimb/isabelle/"
+STEM "/usr/wiss/oheimb/isabelle/"
 
 EXTRACT Tools/8bit/isa-patches/HOLCF/Cfun1.p IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
 EXTRACT Tools/8bit/isa-patches/HOLCF/Cfun1.p2 IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
diff -r de76cee7a30c -r 2fb9659d30ca src/Tools/8bit/xemacs/isa_xemacs
--- a/src/Tools/8bit/xemacs/isa_xemacs	Fri Dec 13 18:25:45 1996 +0100
+++ b/src/Tools/8bit/xemacs/isa_xemacs	Fri Dec 13 18:32:07 1996 +0100
@@ -45,7 +45,7 @@
 
 # set font as XResource
 # needed for versions later than LEmacs 19.9 
-echo "$PREFIX*default.attributeFont: isacr14" | xrdb -merge - >/dev/null
+echo "$PREFIX.default.attributeFont: isacr14" | xrdb -merge - >/dev/null
 
 # pop up isabelle emacs
 $ENAME \