src/HOLCF/Tools/domain/domain_extender.ML
changeset 31023 d027411c9a38
parent 30919 dcf8a7a66bd1
child 31161 a27d4254ff4c
equal deleted inserted replaced
31022:a438b4516dd3 31023:d027411c9a38
    12   val add_domain: string -> (string list * binding * mixfix *
    12   val add_domain: string -> (string list * binding * mixfix *
    13     (binding * (bool * binding option * typ) list * mixfix) list) list
    13     (binding * (bool * binding option * typ) list * mixfix) list) list
    14     -> theory -> theory
    14     -> theory -> theory
    15 end;
    15 end;
    16 
    16 
    17 structure Domain_Extender: DOMAIN_EXTENDER =
    17 structure Domain_Extender :> DOMAIN_EXTENDER =
    18 struct
    18 struct
    19 
    19 
    20 open Domain_Library;
    20 open Domain_Library;
    21 
    21 
    22 (* ----- general testing and preprocessing of constructor list -------------- *)
    22 (* ----- general testing and preprocessing of constructor list -------------- *)