src/HOLCF/fun3.thy
changeset 13897 f62f9a75f685
parent 13896 717bd79b976f
child 13898 9410d2eb9563
--- a/src/HOLCF/fun3.thy	Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title: 	HOLCF/fun3.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Class instance of  => (fun) for class pcpo
-
-*)
-
-Fun3 = Fun2 +
-
-(* default class is still term *)
-
-arities fun  :: (term,pcpo)pcpo		(* Witness fun2.ML *)
-
-rules 
-
-inst_fun_pcpo	"UU::'a=>'b::pcpo = UU_fun"
-
-end
-
-
-