--- 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
Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
Binary file src/Tools/8bit/c-sources/isa2latex/isa2latex has changed
--- 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
Binary file src/Tools/8bit/doc/manual.dvi has changed
--- 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}.
--- 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
--- 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
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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 \