replaced Lift3 by Up3, moving Lift3.p to Up3.p
authoroheimb
Mon, 02 Dec 1996 12:19:56 +0100
changeset 2290 e5c08f8b483b
parent 2289 c53230ac3954
child 2291 fbd14a05fb88
replaced Lift3 by Up3, moving Lift3.p to Up3.p
src/Tools/8bit/isa-patches/HOLCF/HOLCF_ROOT.p
src/Tools/8bit/isa-patches/HOLCF/Lift3.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
--- 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"