src/HOLCF/Porder.thy
changeset 15577 e16da3068ad6
parent 15576 efb95d0d01f7
child 15587 f363e6e080e7
equal deleted inserted replaced
15576:efb95d0d01f7 15577:e16da3068ad6
     7 Conservative extension of theory Porder0 by constant definitions 
     7 Conservative extension of theory Porder0 by constant definitions 
     8 *)
     8 *)
     9 
     9 
    10 header {* Type class of partial orders *}
    10 header {* Type class of partial orders *}
    11 
    11 
    12 theory Porder = Main:
    12 theory Porder
       
    13 imports Main
       
    14 begin
    13 
    15 
    14 	(* introduce a (syntactic) class for the constant << *)
    16 	(* introduce a (syntactic) class for the constant << *)
    15 axclass sq_ord < type
    17 axclass sq_ord < type
    16 
    18 
    17 	(* characteristic constant << for po *)
    19 	(* characteristic constant << for po *)