equal
deleted
inserted
replaced
17 val theory_of: state -> theory |
17 val theory_of: state -> theory |
18 val map_context: (context -> context) -> state -> state |
18 val map_context: (context -> context) -> state -> state |
19 val map_context_result : (context -> 'a * context) -> state -> 'a * state |
19 val map_context_result : (context -> 'a * context) -> state -> 'a * state |
20 val map_contexts: (context -> context) -> state -> state |
20 val map_contexts: (context -> context) -> state -> state |
21 val propagate_ml_env: state -> state |
21 val propagate_ml_env: state -> state |
22 val put_thms: bool -> string * thm list option -> state -> state |
|
23 val the_facts: state -> thm list |
22 val the_facts: state -> thm list |
24 val the_fact: state -> thm |
23 val the_fact: state -> thm |
25 val set_facts: thm list -> state -> state |
24 val set_facts: thm list -> state -> state |
26 val reset_facts: state -> state |
25 val reset_facts: state -> state |
27 val assert_forward: state -> state |
26 val assert_forward: state -> state |
239 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); |
238 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); |
240 |
239 |
241 fun propagate_ml_env state = map_contexts |
240 fun propagate_ml_env state = map_contexts |
242 (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state; |
241 (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state; |
243 |
242 |
244 val put_thms = map_context oo Proof_Context.put_thms; |
|
245 |
|
246 |
243 |
247 (* facts *) |
244 (* facts *) |
248 |
245 |
249 val get_facts = #facts o top; |
246 val get_facts = #facts o top; |
250 |
247 |
258 [thm] => thm |
255 [thm] => thm |
259 | _ => error "Single theorem expected"); |
256 | _ => error "Single theorem expected"); |
260 |
257 |
261 fun put_facts facts = |
258 fun put_facts facts = |
262 map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> |
259 map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> |
263 put_thms true (Auto_Bind.thisN, facts); |
260 map_context (Proof_Context.put_thms true (Auto_Bind.thisN, facts)); |
264 |
261 |
265 val set_facts = put_facts o SOME; |
262 val set_facts = put_facts o SOME; |
266 val reset_facts = put_facts NONE; |
263 val reset_facts = put_facts NONE; |
267 |
264 |
268 fun these_factss more_facts (named_factss, state) = |
265 fun these_factss more_facts (named_factss, state) = |