--- a/src/HOLCF/Fun2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,34 +1,16 @@
-(* Title: HOLCF/fun2.thy
+(* Title: HOLCF/Fun2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance =>::(term,po)po
-Definiton of least element
*)
Fun2 = Fun1 +
(* default class is still term !*)
-(* Witness for the above arity axiom is fun1.ML *)
-
-arities fun :: (term,po)po
-
-consts
- UU_fun :: "'a::term => 'b::pcpo"
-
-rules
-
-(* instance of << for type ['a::term => 'b::po] *)
-
-inst_fun_po "((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
-
-defs
-
-(* The least element in type 'a::term => 'b::pcpo *)
-
-UU_fun_def "UU_fun == (% x.UU)"
+instance fun :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun)
end