src/HOLCF/Porder0.thy
changeset 3310 0ceaad3c3f52
parent 2850 a66196e1668c
child 3323 194ae2e0c193
equal deleted inserted replaced
3309:992a25b24d0d 3310:0ceaad3c3f52
     5 
     5 
     6 Definition of class porder (partial order)
     6 Definition of class porder (partial order)
     7 
     7 
     8 *)
     8 *)
     9 
     9 
    10 Porder0 = Nat +
    10 Porder0 = Arith +
    11 
    11 
    12 (* first the global constant for HOLCF type classes *)
    12 (* first the global constant for HOLCF type classes *)
    13 consts
    13 consts
    14   "less"        :: "['a,'a] => bool"
    14   less        :: "['a,'a] => bool"
    15 
    15 
    16 axclass po < term
    16 axclass po < term
    17         (* class axioms: *)
    17         (* class axioms: *)
    18 ax_refl_less       "less x x"        
    18 ax_refl_less       "less x x"        
    19 ax_antisym_less    "[|less x y; less y x |] ==> x = y"    
    19 ax_antisym_less    "[|less x y; less y x |] ==> x = y"