75 val get_thm: context -> string -> thm |
75 val get_thm: context -> string -> thm |
76 val get_thm_closure: context -> string -> thm |
76 val get_thm_closure: context -> string -> thm |
77 val get_thms: context -> string -> thm list |
77 val get_thms: context -> string -> thm list |
78 val get_thms_closure: context -> string -> thm list |
78 val get_thms_closure: context -> string -> thm list |
79 val cond_extern: context -> string -> xstring |
79 val cond_extern: context -> string -> xstring |
80 val qualified: (context -> context) -> context -> context |
80 val qualified_result: (context -> context * 'a) -> context -> context * 'a |
81 val put_thm: string * thm -> context -> context |
81 val put_thm: string * thm -> context -> context |
82 val put_thms: string * thm list -> context -> context |
82 val put_thms: string * thm list -> context -> context |
83 val put_thmss: (string * thm list) list -> context -> context |
83 val put_thmss: (string * thm list) list -> context -> context |
84 val reset_thms: string -> context -> context |
84 val reset_thms: string -> context -> context |
85 val have_thmss: |
85 val have_thmss: |
92 val export_presume: exporter |
92 val export_presume: exporter |
93 val cert_def: context -> term -> string * term |
93 val cert_def: context -> term -> string * term |
94 val export_def: exporter |
94 val export_def: exporter |
95 val assume: exporter |
95 val assume: exporter |
96 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
96 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
97 -> context -> context * (string * thm list) list |
97 -> context -> context * (bstring * thm list) list |
98 val assume_i: exporter |
98 val assume_i: exporter |
99 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
99 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
100 -> context -> context * (string * thm list) list |
100 -> context -> context * (bstring * thm list) list |
101 val read_vars: context * (string list * string option) -> context * (string list * typ option) |
101 val read_vars: context * (string list * string option) -> context * (string list * typ option) |
102 val cert_vars: context * (string list * typ option) -> context * (string list * typ option) |
102 val cert_vars: context * (string list * typ option) -> context * (string list * typ option) |
103 val fix: (string list * string option) list -> context -> context |
103 val fix: (string list * string option) list -> context -> context |
104 val fix_i: (string list * typ option) list -> context -> context |
104 val fix_i: (string list * typ option) list -> context -> context |
105 val fix_direct: (string list * typ option) list -> context -> context |
105 val fix_direct: (string list * typ option) list -> context -> context |
931 fun cond_extern (Context {thms = (_, space, _), ...}) = NameSpace.cond_extern space; |
931 fun cond_extern (Context {thms = (_, space, _), ...}) = NameSpace.cond_extern space; |
932 |
932 |
933 fun set_qual q = map_context (fn (thy, syntax, data, asms, binds, (_, space, tab), cases, defs) => |
933 fun set_qual q = map_context (fn (thy, syntax, data, asms, binds, (_, space, tab), cases, defs) => |
934 (thy, syntax, data, asms, binds, (q, space, tab), cases, defs)); |
934 (thy, syntax, data, asms, binds, (q, space, tab), cases, defs)); |
935 |
935 |
936 fun qualified f (ctxt as Context {thms, ...}) = |
936 fun qualified_result f (ctxt as Context {thms, ...}) = |
937 ctxt |> set_qual true |> f |> set_qual (#1 thms); |
937 ctxt |> set_qual true |> f |>> set_qual (#1 thms); |
938 |
938 |
939 |
939 |
940 (* put_thm(s) *) |
940 (* put_thm(s) *) |
941 |
941 |
942 fun put_thms ("", _) ctxt = ctxt |
942 fun put_thms ("", _) ctxt = ctxt |