# HG changeset patch
# User oheimb
# Date 849524631 -3600
# Node ID c53230ac395407ddc158c0f0f8a562b8f79a5386
# Parent  16e7a5adb6795578f74815eb04916ebf81fcf931
in Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg

diff -r 16e7a5adb679 -r c53230ac3954 src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Mon Dec 02 10:25:53 1996 +0100
+++ b/src/HOLCF/Cfun1.thy	Mon Dec 02 12:03:51 1996 +0100
@@ -48,26 +48,10 @@
   less_cfun_def         "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
 
 (* start 8bit 1 *)
-types
-
-('a, 'b) "è"          (infixr 5)
-
-syntax
-	Gfabs	:: "('a => 'b)=>('a -> 'b)"	(binder "¤" 10)
-
-translations
-
-(type)  "x è y"	== (type) "x -> y" 
-
 (* end 8bit 1 *)
 
 
 end
 
 (* start 8bit 2 *)
-ML
-val parse_ast_translation = ("¤",    fn asts => Appl (Constant "LAM " :: asts)) ::
-			    parse_ast_translation;
-val print_ast_translation = ("LAM ", fn asts => Appl (Constant "¤"    :: asts)) ::
-			    print_ast_translation;
 (* end 8bit 2 *)
diff -r 16e7a5adb679 -r c53230ac3954 src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
--- a/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg	Mon Dec 02 10:25:53 1996 +0100
+++ b/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg	Mon Dec 02 12:03:51 1996 +0100
@@ -2,6 +2,7 @@
 
 STEM "/usr/stud/oheimb/isabelle/"
 
+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"