src/HOLCF/cfun2.thy
changeset 13896 717bd79b976f
parent 13895 b6105462ccd3
child 13897 f62f9a75f685
--- a/src/HOLCF/cfun2.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title: 	HOLCF/cfun2.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Class Instance ->::(pcpo,pcpo)po
-
-*)
-
-Cfun2 = Cfun1 + 
-
-(* Witness for the above arity axiom is cfun1.ML *)
-arities "->" :: (pcpo,pcpo)po
-
-consts	
-	UU_cfun  :: "'a->'b"
-
-rules
-
-(* instance of << for type ['a -> 'b]  *)
-
-inst_cfun_po	"(op <<)::['a->'b,'a->'b]=>bool = less_cfun"
-
-(* definitions *)
-(* The least element in type 'a->'b *)
-
-UU_cfun_def	"UU_cfun == fabs(% x.UU)"
-
-end
-
-ML
-
-(* ----------------------------------------------------------------------*)
-(* unique setup of print translation for fapp                            *)
-(* ----------------------------------------------------------------------*)
-
-val print_translation = [("fapp",fapptr')];
-
-