--- a/src/Tools/8bit/isa-patches/HOLCF/Holcfb.p Thu Jun 27 12:53:08 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-
-syntax
- "Gmu" :: "[pttrn, bool] => nat" ("(3´_./ _)" 10)
-
-translations
- "´x.P" == "theleast(%x.P)"
-
--- a/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg Thu Jun 27 12:53:08 1996 +0200
+++ b/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg Thu Jun 27 15:19:50 1996 +0200
@@ -2,7 +2,6 @@
STEM "/usr/stud/oheimb/isabelle/"
-ADD Tools/8bit/isa-patches/HOLCF/Holcfb.p IN HOLCF/Holcfb.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1"
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"
--- a/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg Thu Jun 27 12:53:08 1996 +0200
+++ b/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg Thu Jun 27 15:19:50 1996 +0200
@@ -2,7 +2,6 @@
STEM "/usr/stud/oheimb/isabelle/"
-CLEAN IN HOLCF/Holcfb.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"
--- a/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg Thu Jun 27 12:53:08 1996 +0200
+++ b/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg Thu Jun 27 15:19:50 1996 +0200
@@ -2,7 +2,6 @@
STEM "/usr/stud/oheimb/isabelle/"
-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"