26 val hide_space_i: (string * string list) * Comment.text -> theory -> theory |
26 val hide_space_i: (string * string list) * Comment.text -> theory -> theory |
27 val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory |
27 val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory |
28 val add_classes_i: (bclass * class list) list * Comment.text -> theory -> theory |
28 val add_classes_i: (bclass * class list) list * Comment.text -> theory -> theory |
29 val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory |
29 val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory |
30 val add_classrel_i: (class * class) * Comment.text -> theory -> theory |
30 val add_classrel_i: (class * class) * Comment.text -> theory -> theory |
31 val add_defsort: xsort * Comment.text -> theory -> theory |
31 val add_defsort: string * Comment.text -> theory -> theory |
32 val add_defsort_i: sort * Comment.text -> theory -> theory |
32 val add_defsort_i: sort * Comment.text -> theory -> theory |
33 val add_nonterminals: (bstring * Comment.text) list -> theory -> theory |
33 val add_nonterminals: (bstring * Comment.text) list -> theory -> theory |
34 val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list |
34 val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list |
35 -> theory -> theory |
35 -> theory -> theory |
36 val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list |
36 val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list |
37 -> theory -> theory |
37 -> theory -> theory |
38 val add_arities: ((xstring * xsort list * xsort) * Comment.text) list -> theory -> theory |
38 val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory |
39 val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory |
39 val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory |
40 val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory |
40 val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory |
41 val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory |
41 val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory |
42 val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list -> theory -> theory |
42 val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list -> theory -> theory |
43 val add_modesyntax: string * bool -> ((bstring * string * mixfix) * Comment.text) list |
43 val add_modesyntax: string * bool -> ((bstring * string * mixfix) * Comment.text) list |