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;
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