src/HOLCF/ccc1.thy
changeset 752 b89462f9d5f1
parent 625 119391dd1d59
child 1168 74be52691d62
--- a/src/HOLCF/ccc1.thy	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/ccc1.thy	Mon Nov 28 19:48:30 1994 +0100
@@ -10,13 +10,12 @@
 ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix +
 
 consts
-
-	ID 		:: "'a -> 'a"
+	ID 	:: "'a -> 'a"
+	cfcomp	:: "('b->'c)->('a->'b)->'a->'c"
 
-	"@oo"		:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
-	"cop @oo"	:: "('b->'c)->('a->'b)->'a->'c" ("cfcomp")
-
-translations "f1 oo f2" => "cfcomp[f1][f2]"
+syntax	"@oo"	:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
+     
+translations 	"f1 oo f2" == "cfcomp[f1][f2]"
 
 rules