equal
deleted
inserted
replaced
92 val full_name: theory -> bstring -> string |
92 val full_name: theory -> bstring -> string |
93 val full_name_path: theory -> string -> bstring -> string |
93 val full_name_path: theory -> string -> bstring -> string |
94 val declare_name: theory -> string -> NameSpace.T -> NameSpace.T |
94 val declare_name: theory -> string -> NameSpace.T -> NameSpace.T |
95 val syn_of: theory -> Syntax.syntax |
95 val syn_of: theory -> Syntax.syntax |
96 val tsig_of: theory -> Type.tsig |
96 val tsig_of: theory -> Type.tsig |
97 val classes_of: theory -> Sorts.classes |
97 val classes_of: theory -> Sorts.algebra |
98 val arities_of: theory -> Sorts.arities |
|
99 val classes: theory -> class list |
98 val classes: theory -> class list |
100 val super_classes: theory -> class -> class list |
99 val super_classes: theory -> class -> class list |
101 val defaultS: theory -> sort |
100 val defaultS: theory -> sort |
102 val subsort: theory -> sort * sort -> bool |
101 val subsort: theory -> sort * sort -> bool |
103 val of_sort: theory -> typ * sort -> bool |
102 val of_sort: theory -> typ * sort -> bool |
265 |
264 |
266 |
265 |
267 (* type signature *) |
266 (* type signature *) |
268 |
267 |
269 val tsig_of = #tsig o rep_sg; |
268 val tsig_of = #tsig o rep_sg; |
270 val classes_of = snd o #classes o Type.rep_tsig o tsig_of; |
269 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; |
271 val arities_of = #arities o Type.rep_tsig o tsig_of; |
270 val classes = Sorts.classes o classes_of; |
272 val classes = Type.classes o tsig_of; |
271 val super_classes = Sorts.super_classes o classes_of; |
273 val super_classes = Graph.imm_succs o classes_of; |
|
274 val defaultS = Type.defaultS o tsig_of; |
272 val defaultS = Type.defaultS o tsig_of; |
275 val subsort = Type.subsort o tsig_of; |
273 val subsort = Type.subsort o tsig_of; |
276 val of_sort = Type.of_sort o tsig_of; |
274 val of_sort = Type.of_sort o tsig_of; |
277 val witness_sorts = Type.witness_sorts o tsig_of; |
275 val witness_sorts = Type.witness_sorts o tsig_of; |
278 val universal_witness = Type.universal_witness o tsig_of; |
276 val universal_witness = Type.universal_witness o tsig_of; |