# HG changeset patch
# User oheimb
# Date 849525596 -3600
# Node ID e5c08f8b483b3c1962b4ca1c35da1ef118fe5bef
# Parent  c53230ac395407ddc158c0f0f8a562b8f79a5386
replaced Lift3 by Up3, moving Lift3.p to Up3.p

diff -r c53230ac3954 -r e5c08f8b483b src/Tools/8bit/isa-patches/HOLCF/HOLCF_ROOT.p
--- 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";
diff -r c53230ac3954 -r e5c08f8b483b src/Tools/8bit/isa-patches/HOLCF/Lift3.p
--- 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"
-
diff -r c53230ac3954 -r e5c08f8b483b src/Tools/8bit/isa-patches/HOLCF/Up3.p
--- /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"
+
diff -r c53230ac3954 -r e5c08f8b483b src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg
--- 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" 
diff -r c53230ac3954 -r e5c08f8b483b src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
--- 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" 
diff -r c53230ac3954 -r e5c08f8b483b src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg
--- 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"