src/HOLCF/Porder0.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3323 194ae2e0c193
child 7661 8c3190b173aa
permissions -rw-r--r--
made tutorial first;
     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 = Arith +
    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