equal
deleted
inserted
replaced
34 sig |
34 sig |
35 include BASIC_THEORY |
35 include BASIC_THEORY |
36 val apply: (theory -> theory) list -> theory -> theory |
36 val apply: (theory -> theory) list -> theory -> theory |
37 val axiomK: string |
37 val axiomK: string |
38 val oracleK: string |
38 val oracleK: string |
39 (*theory extendsion primitives*) |
39 (*theory extension primitives*) |
40 val add_classes: (bclass * xclass list) list -> theory -> theory |
40 val add_classes: (bclass * xclass list) list -> theory -> theory |
41 val add_classes_i: (bclass * class list) list -> theory -> theory |
41 val add_classes_i: (bclass * class list) list -> theory -> theory |
42 val add_classrel: (xclass * xclass) list -> theory -> theory |
42 val add_classrel: (xclass * xclass) list -> theory -> theory |
43 val add_classrel_i: (class * class) list -> theory -> theory |
43 val add_classrel_i: (class * class) list -> theory -> theory |
44 val add_defsort: xsort -> theory -> theory |
44 val add_defsort: xsort -> theory -> theory |