--- a/src/Tools/8bit/isa-patches/HOLCF/HOLCF_ROOT.p Mon Dec 02 12:03:51 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/HOLCF_ROOT.p Mon Dec 02 12:19:56 1996 +0100
@@ -1,2 +1,2 @@
val banner =
- "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
+ "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
--- a/src/Tools/8bit/isa-patches/HOLCF/Lift3.p Mon Dec 02 12:03:51 1996 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-translations
-"case l of up`x => t1" == "lift`(¤x.t1)`l"
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/isa-patches/HOLCF/Up3.p Mon Dec 02 12:19:56 1996 +0100
@@ -0,0 +1,3 @@
+translations
+"case l of up`x => t1" == "lift`(¤x.t1)`l"
+
--- a/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg Mon Dec 02 12:03:51 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg Mon Dec 02 12:19:56 1996 +0100
@@ -5,7 +5,7 @@
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"
ADD Tools/8bit/isa-patches/HOLCF/Cprod3.p IN HOLCF/Cprod3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-ADD Tools/8bit/isa-patches/HOLCF/Lift3.p IN HOLCF/Lift3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+ADD Tools/8bit/isa-patches/HOLCF/Up3.p IN HOLCF/Up3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
ADD Tools/8bit/isa-patches/HOLCF/Pcpo.p IN HOLCF/Pcpo.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
ADD Tools/8bit/isa-patches/HOLCF/Porder.p IN HOLCF/Porder.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
ADD Tools/8bit/isa-patches/HOLCF/Porder0.p IN HOLCF/Porder0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
--- a/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg Mon Dec 02 12:03:51 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg Mon Dec 02 12:19:56 1996 +0100
@@ -5,7 +5,7 @@
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"
CLEAN IN HOLCF/Cprod3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-CLEAN IN HOLCF/Lift3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+CLEAN IN HOLCF/Up3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
CLEAN IN HOLCF/Pcpo.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
CLEAN IN HOLCF/Porder.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
CLEAN IN HOLCF/Porder0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
--- a/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg Mon Dec 02 12:03:51 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg Mon Dec 02 12:19:56 1996 +0100
@@ -5,7 +5,7 @@
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"
EXTRACT Tools/8bit/isa-patches/HOLCF/Cprod3.p IN HOLCF/Cprod3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT Tools/8bit/isa-patches/HOLCF/Lift3.p IN HOLCF/Lift3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Up3.p IN HOLCF/Up3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
EXTRACT Tools/8bit/isa-patches/HOLCF/Pcpo.p IN HOLCF/Pcpo.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
EXTRACT Tools/8bit/isa-patches/HOLCF/Porder.p IN HOLCF/Porder.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
EXTRACT Tools/8bit/isa-patches/HOLCF/Porder0.p IN HOLCF/Porder0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"