31 |
31 |
32 signature THEORY = |
32 signature THEORY = |
33 sig |
33 sig |
34 include BASIC_THEORY |
34 include BASIC_THEORY |
35 (*theory extendsion primitives*) |
35 (*theory extendsion primitives*) |
36 val add_classes : (class * class list) list -> theory -> theory |
36 val add_classes : (xclass * xclass list) list -> theory -> theory |
37 val add_classes_i : (class * class list) list -> theory -> theory |
37 val add_classes_i : (xclass * class list) list -> theory -> theory |
38 val add_classrel : (class * class) list -> theory -> theory |
38 val add_classrel : (xclass * xclass) list -> theory -> theory |
39 val add_classrel_i : (class * class) list -> theory -> theory |
39 val add_classrel_i : (class * class) list -> theory -> theory |
40 val add_defsort : sort -> theory -> theory |
40 val add_defsort : xsort -> theory -> theory |
41 val add_defsort_i : sort -> theory -> theory |
41 val add_defsort_i : sort -> theory -> theory |
42 val add_types : (string * int * mixfix) list -> theory -> theory |
42 val add_types : (xstring * int * mixfix) list -> theory -> theory |
43 val add_tyabbrs : (string * string list * string * mixfix) list |
43 val add_tyabbrs : (xstring * string list * string * mixfix) list |
44 -> theory -> theory |
44 -> theory -> theory |
45 val add_tyabbrs_i : (string * string list * typ * mixfix) list |
45 val add_tyabbrs_i : (xstring * string list * typ * mixfix) list |
46 -> theory -> theory |
46 -> theory -> theory |
47 val add_arities : (string * sort list * sort) list -> theory -> theory |
47 val add_arities : (xstring * xsort list * xsort) list -> theory -> theory |
48 val add_arities_i : (string * sort list * sort) list -> theory -> theory |
48 val add_arities_i : (string * sort list * sort) list -> theory -> theory |
49 val add_consts : (string * string * mixfix) list -> theory -> theory |
49 val add_consts : (xstring * string * mixfix) list -> theory -> theory |
50 val add_consts_i : (string * typ * mixfix) list -> theory -> theory |
50 val add_consts_i : (xstring * typ * mixfix) list -> theory -> theory |
51 val add_syntax : (string * string * mixfix) list -> theory -> theory |
51 val add_syntax : (xstring * string * mixfix) list -> theory -> theory |
52 val add_syntax_i : (string * typ * mixfix) list -> theory -> theory |
52 val add_syntax_i : (xstring * typ * mixfix) list -> theory -> theory |
53 val add_modesyntax : string * bool -> (string * string * mixfix) list -> theory -> theory |
53 val add_modesyntax : string * bool -> (xstring * string * mixfix) list -> theory -> theory |
54 val add_modesyntax_i : string * bool -> (string * typ * mixfix) list -> theory -> theory |
54 val add_modesyntax_i : string * bool -> (xstring * typ * mixfix) list -> theory -> theory |
55 val add_trfuns : |
55 val add_trfuns : |
56 (string * (Syntax.ast list -> Syntax.ast)) list * |
56 (string * (Syntax.ast list -> Syntax.ast)) list * |
57 (string * (term list -> term)) list * |
57 (string * (term list -> term)) list * |
58 (string * (term list -> term)) list * |
58 (string * (term list -> term)) list * |
59 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
59 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
61 (string * (typ -> term list -> term)) list -> theory -> theory |
61 (string * (typ -> term list -> term)) list -> theory -> theory |
62 val add_tokentrfuns: |
62 val add_tokentrfuns: |
63 (string * string * (string -> string * int)) list -> theory -> theory |
63 (string * string * (string -> string * int)) list -> theory -> theory |
64 val add_trrules : (string * string)Syntax.trrule list -> theory -> theory |
64 val add_trrules : (string * string)Syntax.trrule list -> theory -> theory |
65 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
65 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
66 val add_axioms : (string * string) list -> theory -> theory |
66 val add_axioms : (xstring * string) list -> theory -> theory |
67 val add_axioms_i : (string * term) list -> theory -> theory |
67 val add_axioms_i : (xstring * term) list -> theory -> theory |
68 val add_defs : (string * string) list -> theory -> theory |
68 val add_defs : (xstring * string) list -> theory -> theory |
69 val add_defs_i : (string * term) list -> theory -> theory |
69 val add_defs_i : (xstring * term) list -> theory -> theory |
70 val add_path : string -> theory -> theory |
70 val add_path : string -> theory -> theory |
71 val add_space : string * string list -> theory -> theory |
71 val add_space : string * xstring list -> theory -> theory |
72 val add_name : string -> theory -> theory |
72 val add_name : string -> theory -> theory |
73 |
73 |
74 val set_oracle : (Sign.sg * exn -> term) -> theory -> theory |
74 val set_oracle : (Sign.sg * exn -> term) -> theory -> theory |
75 |
75 |
76 val merge_thy_list : bool -> theory list -> theory |
76 val merge_thy_list : bool -> theory list -> theory |