38 (*theory extension primitives*) |
38 (*theory extension primitives*) |
39 val add_classes: (bclass * xclass list) list -> theory -> theory |
39 val add_classes: (bclass * xclass list) list -> theory -> theory |
40 val add_classes_i: (bclass * class list) list -> theory -> theory |
40 val add_classes_i: (bclass * class list) list -> theory -> theory |
41 val add_classrel: (xclass * xclass) list -> theory -> theory |
41 val add_classrel: (xclass * xclass) list -> theory -> theory |
42 val add_classrel_i: (class * class) list -> theory -> theory |
42 val add_classrel_i: (class * class) list -> theory -> theory |
43 val add_defsort: xsort -> theory -> theory |
43 val add_defsort: string -> theory -> theory |
44 val add_defsort_i: sort -> theory -> theory |
44 val add_defsort_i: sort -> theory -> theory |
45 val add_types: (bstring * int * mixfix) list -> theory -> theory |
45 val add_types: (bstring * int * mixfix) list -> theory -> theory |
46 val add_nonterminals: bstring list -> theory -> theory |
46 val add_nonterminals: bstring list -> theory -> theory |
47 val add_tyabbrs: (bstring * string list * string * mixfix) list |
47 val add_tyabbrs: (bstring * string list * string * mixfix) list |
48 -> theory -> theory |
48 -> theory -> theory |
49 val add_tyabbrs_i: (bstring * string list * typ * mixfix) list |
49 val add_tyabbrs_i: (bstring * string list * typ * mixfix) list |
50 -> theory -> theory |
50 -> theory -> theory |
51 val add_arities: (xstring * xsort list * xsort) list -> theory -> theory |
51 val add_arities: (xstring * string list * string) list -> theory -> theory |
52 val add_arities_i: (string * sort list * sort) list -> theory -> theory |
52 val add_arities_i: (string * sort list * sort) list -> theory -> theory |
53 val add_consts: (bstring * string * mixfix) list -> theory -> theory |
53 val add_consts: (bstring * string * mixfix) list -> theory -> theory |
54 val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory |
54 val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory |
55 val add_syntax: (bstring * string * mixfix) list -> theory -> theory |
55 val add_syntax: (bstring * string * mixfix) list -> theory -> theory |
56 val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory |
56 val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory |