--- a/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg Wed Jun 26 17:38:34 1996 +0200
+++ b/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg Wed Jun 26 17:45:32 1996 +0200
@@ -2,18 +2,18 @@
STEM "/usr/stud/oheimb/isabelle/"
-EXTRACT 8bit/isa-patches/HOLCF/Holcfb.p IN HOLCF/Holcfb.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Cfun1.p IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Cfun1.p2 IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2"
-EXTRACT 8bit/isa-patches/HOLCF/Cprod3.p IN HOLCF/Cprod3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Lift3.p IN HOLCF/Lift3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Pcpo.p IN HOLCF/Pcpo.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Porder.p IN HOLCF/Porder.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Porder0.p IN HOLCF/Porder0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/HOLCF_ROOT.p IN HOLCF/ROOT.ML BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Sprod0.p IN HOLCF/Sprod0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Sprod3.p IN HOLCF/Sprod3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Ssum0.p IN HOLCF/Ssum0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Ssum3.p IN HOLCF/Ssum3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
-EXTRACT 8bit/isa-patches/HOLCF/Tr1.p IN HOLCF/Tr1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Holcfb.p IN HOLCF/Holcfb.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+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/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"
+EXTRACT Tools/8bit/isa-patches/HOLCF/HOLCF_ROOT.p IN HOLCF/ROOT.ML BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Sprod0.p IN HOLCF/Sprod0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Sprod3.p IN HOLCF/Sprod3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Ssum0.p IN HOLCF/Ssum0.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Ssum3.p IN HOLCF/Ssum3.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
+EXTRACT Tools/8bit/isa-patches/HOLCF/Tr1.p IN HOLCF/Tr1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"