patches for Holcfb.thy removed
authoroheimb
Thu, 27 Jun 1996 15:19:50 +0200
changeset 1833 59f5256d8dd2
parent 1832 79dd1433867c
child 1834 c780a4f39454
patches for Holcfb.thy removed
src/Tools/8bit/isa-patches/HOLCF/Holcfb.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/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"