equal
deleted
inserted
replaced
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 |