equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature BASIC_SIMPLIFIER = |
8 signature BASIC_SIMPLIFIER = |
9 sig |
9 sig |
10 include BASIC_RAW_SIMPLIFIER |
10 include BASIC_RAW_SIMPLIFIER |
|
11 val map_simpset_local: (simpset -> simpset) -> Proof.context -> Proof.context |
11 val change_simpset: (simpset -> simpset) -> unit |
12 val change_simpset: (simpset -> simpset) -> unit |
12 val global_simpset_of: theory -> simpset |
13 val global_simpset_of: theory -> simpset |
13 val Addsimprocs: simproc list -> unit |
14 val Addsimprocs: simproc list -> unit |
14 val Delsimprocs: simproc list -> unit |
15 val Delsimprocs: simproc list -> unit |
15 val simpset_of: Proof.context -> simpset |
16 val simpset_of: Proof.context -> simpset |
134 val cong_del = attrib (op delcongs); |
135 val cong_del = attrib (op delcongs); |
135 |
136 |
136 |
137 |
137 (* global simpset *) |
138 (* global simpset *) |
138 |
139 |
139 fun map_simpset f = Context.theory_map (map_ss f); |
140 fun map_simpset f = Context.theory_map (map_ss f); (* FIXME global *) |
140 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f)); |
141 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f)); |
141 fun global_simpset_of thy = |
142 fun global_simpset_of thy = |
142 Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy)); |
143 Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy)); |
143 |
144 |
144 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args); |
145 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args); |
145 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args); |
146 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args); |
146 |
147 |
147 |
148 |
148 (* local simpset *) |
149 (* local simpset *) |
149 |
150 |
|
151 fun map_simpset_local f = Context.proof_map (map_ss f); |
150 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt)); |
152 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt)); |
151 |
153 |
152 val _ = ML_Antiquote.value "simpset" |
154 val _ = ML_Antiquote.value "simpset" |
153 (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())"); |
155 (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())"); |
154 |
156 |