35 sig |
35 sig |
36 include BASIC_THEORY |
36 include BASIC_THEORY |
37 val thmK : string |
37 val thmK : string |
38 val oracleK : string |
38 val oracleK : string |
39 (*theory extendsion primitives*) |
39 (*theory extendsion primitives*) |
40 val add_classes : (xclass * xclass list) list -> theory -> theory |
40 val add_classes : (rclass * xclass list) list -> theory -> theory |
41 val add_classes_i : (xclass * class list) list -> theory -> theory |
41 val add_classes_i : (rclass * 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 |
45 val add_defsort_i : sort -> theory -> theory |
45 val add_defsort_i : sort -> theory -> theory |
46 val add_types : (xstring * int * mixfix) list -> theory -> theory |
46 val add_types : (rstring * int * mixfix) list -> theory -> theory |
47 val add_tyabbrs : (xstring * string list * string * mixfix) list |
47 val add_tyabbrs : (rstring * string list * string * mixfix) list |
48 -> theory -> theory |
48 -> theory -> theory |
49 val add_tyabbrs_i : (xstring * string list * typ * mixfix) list |
49 val add_tyabbrs_i : (rstring * 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 * xsort list * xsort) 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 : (xstring * string * mixfix) list -> theory -> theory |
53 val add_consts : (rstring * string * mixfix) list -> theory -> theory |
54 val add_consts_i : (xstring * typ * mixfix) list -> theory -> theory |
54 val add_consts_i : (rstring * typ * mixfix) list -> theory -> theory |
55 val add_syntax : (xstring * string * mixfix) list -> theory -> theory |
55 val add_syntax : (rstring * string * mixfix) list -> theory -> theory |
56 val add_syntax_i : (xstring * typ * mixfix) list -> theory -> theory |
56 val add_syntax_i : (rstring * typ * mixfix) list -> theory -> theory |
57 val add_modesyntax : string * bool -> (xstring * string * mixfix) list -> theory -> theory |
57 val add_modesyntax : string * bool -> (rstring * string * mixfix) list -> theory -> theory |
58 val add_modesyntax_i : string * bool -> (xstring * typ * mixfix) list -> theory -> theory |
58 val add_modesyntax_i : string * bool -> (rstring * typ * mixfix) list -> theory -> theory |
59 val add_trfuns : |
59 val add_trfuns : |
60 (string * (Syntax.ast list -> Syntax.ast)) list * |
60 (string * (Syntax.ast list -> Syntax.ast)) list * |
61 (string * (term list -> term)) list * |
61 (string * (term list -> term)) list * |
62 (string * (term list -> term)) list * |
62 (string * (term list -> term)) list * |
63 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
63 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
64 val add_trfunsT : |
64 val add_trfunsT : |
65 (string * (typ -> term list -> term)) list -> theory -> theory |
65 (string * (typ -> term list -> term)) list -> theory -> theory |
66 val add_tokentrfuns: |
66 val add_tokentrfuns: |
67 (string * string * (string -> string * int)) list -> theory -> theory |
67 (string * string * (string -> string * int)) list -> theory -> theory |
68 val add_trrules : (string * string)Syntax.trrule list -> theory -> theory |
68 val add_trrules : (string * string) Syntax.trrule list -> theory -> theory |
69 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
69 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
70 val add_axioms : (xstring * string) list -> theory -> theory |
70 val add_axioms : (rstring * string) list -> theory -> theory |
71 val add_axioms_i : (xstring * term) list -> theory -> theory |
71 val add_axioms_i : (rstring * term) list -> theory -> theory |
72 val add_oracle : string * (Sign.sg * exn -> term) -> theory -> theory |
72 val add_oracle : rstring * (Sign.sg * exn -> term) -> theory -> theory |
73 val add_defs : (xstring * string) list -> theory -> theory |
73 val add_defs : (rstring * string) list -> theory -> theory |
74 val add_defs_i : (xstring * term) list -> theory -> theory |
74 val add_defs_i : (rstring * term) list -> theory -> theory |
75 val add_path : string -> theory -> theory |
75 val add_path : string -> theory -> theory |
76 val add_space : string * string list -> theory -> theory |
76 val add_space : string * string list -> theory -> theory |
77 val add_name : string -> theory -> theory |
77 val add_name : string -> theory -> theory |
78 val init_data : string * exn * (exn -> exn) * (exn * exn -> exn) * |
78 val init_data : string * exn * (exn -> exn) * (exn * exn -> exn) * |
79 (string -> exn -> unit) -> theory -> theory |
79 (string -> exn -> unit) -> theory -> theory |