71 sig |
71 sig |
72 include BASIC_RAW_SIMPLIFIER |
72 include BASIC_RAW_SIMPLIFIER |
73 exception SIMPLIFIER of string * thm list |
73 exception SIMPLIFIER of string * thm list |
74 type trace_ops |
74 type trace_ops |
75 val set_trace_ops: trace_ops -> theory -> theory |
75 val set_trace_ops: trace_ops -> theory -> theory |
76 val internal_ss: simpset -> |
76 val subgoal_tac: Proof.context -> int -> tactic |
77 {congs: (cong_name * thm) list * cong_name list, |
77 val loop_tac: Proof.context -> int -> tactic |
78 procs: proc Net.net, |
78 val solvers: Proof.context -> solver list * solver list |
79 mk_rews: |
|
80 {mk: Proof.context -> thm -> thm list, |
|
81 mk_cong: Proof.context -> thm -> thm, |
|
82 mk_sym: Proof.context -> thm -> thm option, |
|
83 mk_eq_True: Proof.context -> thm -> thm option, |
|
84 reorient: Proof.context -> term list -> term -> term -> bool}, |
|
85 term_ord: term ord, |
|
86 subgoal_tac: Proof.context -> int -> tactic, |
|
87 loop_tacs: (string * (Proof.context -> int -> tactic)) list, |
|
88 solvers: solver list * solver list} |
|
89 val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic |
79 val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic |
90 val prems_of: Proof.context -> thm list |
80 val prems_of: Proof.context -> thm list |
91 val add_simp: thm -> Proof.context -> Proof.context |
81 val add_simp: thm -> Proof.context -> Proof.context |
92 val del_simp: thm -> Proof.context -> Proof.context |
82 val del_simp: thm -> Proof.context -> Proof.context |
93 val flip_simp: thm -> Proof.context -> Proof.context |
83 val flip_simp: thm -> Proof.context -> Proof.context |
380 fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f; |
370 fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f; |
381 |
371 |
382 val clear_simpset = |
372 val clear_simpset = |
383 map_simpset (fn Simpset ({depth, ...}, {mk_rews, term_ord, subgoal_tac, solvers, ...}) => |
373 map_simpset (fn Simpset ({depth, ...}, {mk_rews, term_ord, subgoal_tac, solvers, ...}) => |
384 init_ss depth mk_rews term_ord subgoal_tac solvers); |
374 init_ss depth mk_rews term_ord subgoal_tac solvers); |
|
375 |
|
376 |
|
377 (* accessors for tactis *) |
|
378 |
|
379 fun subgoal_tac ctxt = (#subgoal_tac o internal_ss o simpset_of) ctxt ctxt; |
|
380 |
|
381 fun loop_tac ctxt = |
|
382 FIRST' (map (fn (_, tac) => tac ctxt) (rev ((#loop_tacs o internal_ss o simpset_of) ctxt))); |
|
383 |
|
384 val solvers = #solvers o internal_ss o simpset_of |
385 |
385 |
386 |
386 |
387 (* simp depth *) |
387 (* simp depth *) |
388 |
388 |
389 (* |
389 (* |