diff -r 717bd79b976f -r f62f9a75f685 src/HOLCF/pcpo.thy
--- a/src/HOLCF/pcpo.thy	Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title: 	HOLCF/pcpo.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Definition of class pcpo (pointed complete partial order)
-
-The prototype theory for this class is porder.thy 
-
-*)
-
-Pcpo = Porder +
-
-(* Introduction of new class. The witness is type void. *)
-
-classes pcpo < po
-
-(* default class is still term *)
-(* void is the prototype in pcpo *)
-
-arities void :: pcpo
-
-consts	
-	UU	::	"'a::pcpo"		(* UU is the least element *)
-rules
-
-(* class axioms: justification is theory Porder *)
-
-minimal		"UU << x"			(* witness is minimal_void *)
-
-cpo		"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
-						(* witness is cpo_void     *)
-						(* needs explicit type     *)
-
-(* instance of UU for the prototype void *)
-
-inst_void_pcpo	"UU::void = UU_void"
-
-end