--- a/src/HOLCF/fun1.thy Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: HOLCF/fun1.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-
-Definition of the partial ordering for the type of all functions => (fun)
-
-REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!
-
-*)
-
-Fun1 = Pcpo +
-
-(* default class is still term *)
-
-consts
- less_fun :: "['a=>'b::po,'a=>'b] => bool"
-
-rules
- (* definition of the ordering less_fun *)
- (* in fun1.ML it is proved that less_fun is a po *)
-
- less_fun_def "less_fun(f1,f2) == ! x. f1(x) << f2(x)"
-
-end
-
-
-
-