Quot/quotient_info.ML
changeset 850 3c6f8a4074c4
parent 836 c2501b2b262a
child 862 09ec51d50fc6
equal deleted inserted replaced
849:fa2b4b7af755 850:3c6f8a4074c4
    63 structure Quotient_Info: QUOTIENT_INFO =
    63 structure Quotient_Info: QUOTIENT_INFO =
    64 struct
    64 struct
    65 
    65 
    66 exception NotFound
    66 exception NotFound
    67 
    67 
    68 (*******************)
    68 
    69 (* data containers *)
    69 (** data containers **)
    70 (*******************)
       
    71 
    70 
    72 (* info about map- and rel-functions for a type *)
    71 (* info about map- and rel-functions for a type *)
    73 type maps_info = {mapfun: string, relmap: string}
    72 type maps_info = {mapfun: string, relmap: string}
    74 
    73 
    75 structure MapsData = Theory_Data
    74 structure MapsData = Theory_Data