src/HOLCF/Porder0.thy
author wenzelm
Thu Sep 30 16:16:56 1999 +0200 (1999-09-30)
changeset 7661 8c3190b173aa
parent 3323 194ae2e0c193
child 12030 46d57d0290a2
permissions -rw-r--r--
depend on Main;
     1 (*  Title:      HOLCF/Porder0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Definition of class porder (partial order)
     7 
     8 *)
     9 
    10 Porder0 = Main +
    11 
    12 	(* introduce a (syntactic) class for the constant << *)
    13 axclass sq_ord<term
    14 
    15 	(* characteristic constant << for po *)
    16 consts
    17   "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
    18 
    19 syntax (symbols)
    20   "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
    21 
    22 axclass po < sq_ord
    23         (* class axioms: *)
    24 refl_less       "x << x"        
    25 antisym_less    "[|x << y; y << x |] ==> x = y"    
    26 trans_less      "[|x << y; y << z |] ==> x << z"
    27  
    28 end 
    29 
    30