diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Porder.thy	Thu Mar 24 13:36:34 1994 +0100
@@ -3,25 +3,13 @@
     Author: 	Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Definition of class porder (partial order)
-
-The prototype theory for this class is void.thy 
+Conservative extension of theory Porder0 by constant definitions 
 
 *)
 
-Porder = Void +
-
-(* Introduction of new class. The witness is type void. *)
-
-classes po < term
+Porder = Porder0 +
 
-(* default type is still term ! *)
-(* void is the prototype in po *)
-
-arities void :: po
-
-consts	"<<"	::	"['a,'a::po] => bool"	(infixl 55)
-
+consts	
 	"<|"	::	"['a set,'a::po] => bool"	(infixl 55)
 	"<<|"	::	"['a set,'a::po] => bool"	(infixl 55)
 	lub	::	"'a set => 'a::po"
@@ -32,21 +20,6 @@
 
 rules
 
-(* class axioms: justification is theory Void *)
-
-refl_less	"x << x"	
-				(* witness refl_less_void    *)
-
-antisym_less	"[|x<<y ; y<<x |] ==> x = y"	
-				(* witness antisym_less_void *)
-
-trans_less	"[|x<<y ; y<<z |] ==> x<<z"
-				(* witness trans_less_void   *)
-
-(* instance of << for the prototype void *)
-
-inst_void_po	"(op <<)::[void,void]=>bool = less_void"
-
 (* class definitions *)
 
 is_ub		"S  <| x == ! y.y:S --> y<<x"
@@ -57,11 +30,9 @@
 (* Arbitrary chains are total orders    *)                  
 is_tord		"is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
 
-
 (* Here we use countable chains and I prefer to code them as functions! *)
 is_chain	"is_chain(F) == (! i.F(i) << F(Suc(i)))"
 
-
 (* finite chains, needed for monotony of continouous functions *)
 
 max_in_chain_def "max_in_chain(i,C) == ! j. i <= j --> C(i) = C(j)"