src/HOLCF/Porder0.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3323 194ae2e0c193
child 7661 8c3190b173aa
permissions -rw-r--r--
tidying
slotosch@2640
     1
(*  Title:      HOLCF/Porder0.thy
nipkow@298
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@298
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@298
     5
nipkow@298
     6
Definition of class porder (partial order)
nipkow@298
     7
nipkow@298
     8
*)
nipkow@298
     9
nipkow@3310
    10
Porder0 = Arith +
nipkow@298
    11
slotosch@3323
    12
	(* introduce a (syntactic) class for the constant << *)
slotosch@3323
    13
axclass sq_ord<term
nipkow@298
    14
slotosch@3323
    15
	(* characteristic constant << for po *)
oheimb@2394
    16
consts
slotosch@3323
    17
  "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
oheimb@2394
    18
oheimb@2394
    19
syntax (symbols)
slotosch@3323
    20
  "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
nipkow@298
    21
slotosch@3323
    22
axclass po < sq_ord
slotosch@3323
    23
        (* class axioms: *)
slotosch@3323
    24
refl_less       "x << x"        
slotosch@3323
    25
antisym_less    "[|x << y; y << x |] ==> x = y"    
slotosch@3323
    26
trans_less      "[|x << y; y << z |] ==> x << z"
slotosch@3323
    27
 
nipkow@298
    28
end 
regensbu@1274
    29
regensbu@1274
    30