src/HOLCF/Porder0.thy
author nipkow
Fri, 23 May 1997 09:20:35 +0200
changeset 3310 0ceaad3c3f52
parent 2850 a66196e1668c
child 3323 194ae2e0c193
permissions -rw-r--r--
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