src/HOLCF/Porder0.thy

Base theory is now Arith, not Nat. (because all datatypes now require Arith).

(*  Title:      HOLCF/Porder0.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Definition of class porder (partial order)

*)

Porder0 = Arith +

(* first the global constant for HOLCF type classes *)
consts
  less        :: "['a,'a] => bool"

axclass po < term
        (* class axioms: *)
ax_refl_less       "less x x"        
ax_antisym_less    "[|less x y; less y x |] ==> x = y"    
ax_trans_less      "[|less x y; less y z |] ==> less x z"
 
	(* characteristic constant << on po *)
consts
  "<<"          :: "['a,'a::po] => bool"        (infixl 55)

syntax (symbols)
  "op <<"       :: "['a,'a::po] => bool"        (infixl "\\<sqsubseteq>" 55)

defs
po_def             "(op <<) == less"
end