equal
deleted
inserted
replaced
61 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
61 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
62 val add_trfunsT: |
62 val add_trfunsT: |
63 (string * (bool -> typ -> term list -> term)) list -> theory -> theory |
63 (string * (bool -> typ -> term list -> term)) list -> theory -> theory |
64 val add_tokentrfuns: |
64 val add_tokentrfuns: |
65 (string * string * (string -> string * int)) list -> theory -> theory |
65 (string * string * (string -> string * int)) list -> theory -> theory |
66 val add_trrules: (string * string) Syntax.trrule list -> theory -> theory |
66 val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
67 val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory |
67 val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory |
68 val add_axioms: (bstring * string) list -> theory -> theory |
68 val add_axioms: (bstring * string) list -> theory -> theory |
69 val add_axioms_i: (bstring * term) list -> theory -> theory |
69 val add_axioms_i: (bstring * term) list -> theory -> theory |
70 val add_oracle: bstring * (Sign.sg * object -> term) -> theory -> theory |
70 val add_oracle: bstring * (Sign.sg * object -> term) -> theory -> theory |
71 val add_defs: (bstring * string) list -> theory -> theory |
71 val add_defs: (bstring * string) list -> theory -> theory |