--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/porder0.thy Thu Mar 24 13:43:45 1994 +0100
@@ -0,0 +1,42 @@
+(* Title: HOLCF/porder0.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Definition of class porder (partial order)
+
+The prototype theory for this class is void.thy
+
+*)
+
+Porder0 = Void +
+
+(* Introduction of new class. The witness is type void. *)
+
+classes po < term
+
+(* default type is still term ! *)
+(* void is the prototype in po *)
+
+arities void :: po
+
+consts "<<" :: "['a,'a::po] => bool" (infixl 55)
+
+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"
+
+end