# HG changeset patch
# User oheimb
# Date 835881590 -7200
# Node ID 59f5256d8dd2ab73c3b058411ad08d635487e983
# Parent  79dd1433867c8e0eccb652728dc49e2222a139d5
patches for Holcfb.thy removed

diff -r 79dd1433867c -r 59f5256d8dd2 src/Tools/8bit/isa-patches/HOLCF/Holcfb.p
--- 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)"
-
diff -r 79dd1433867c -r 59f5256d8dd2 src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg
--- 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" 
diff -r 79dd1433867c -r 59f5256d8dd2 src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
--- 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" 
diff -r 79dd1433867c -r 59f5256d8dd2 src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg
--- 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"