--- a/src/HOLCF/Cfun2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/cfun2.thy
+(* Title: HOLCF/Cfun2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -9,22 +9,6 @@
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"
-
-defs
-(* The least element in type 'a->'b *)
-
-UU_cfun_def "UU_cfun == fabs(% x.UU)"
+instance "->"::(pcpo,pcpo)po (refl_less_cfun,antisym_less_cfun,trans_less_cfun)
end
-