equal
deleted
inserted
replaced
24 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
24 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
25 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
25 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
26 val args_parser: (thm list * string list) context_parser |
26 val args_parser: (thm list * string list) context_parser |
27 |
27 |
28 val trace_eqvt: bool Config.T |
28 val trace_eqvt: bool Config.T |
29 val setup: theory -> theory |
|
30 end; |
29 end; |
31 |
30 |
32 (* |
31 (* |
33 |
32 |
34 - eqvt_tac and eqvt_rule take a list of theorems which |
33 - eqvt_tac and eqvt_rule take a list of theorems which |
93 post_thms = @{thms permute_pure}, |
92 post_thms = @{thms permute_pure}, |
94 excluded = [] } |
93 excluded = [] } |
95 |
94 |
96 |
95 |
97 (* tracing infrastructure *) |
96 (* tracing infrastructure *) |
98 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
97 val trace_eqvt = Attrib.setup_config_bool @{binding "trace_eqvt"} (K false); |
99 |
98 |
100 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
99 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
101 |
100 |
102 fun trace_msg ctxt result = |
101 fun trace_msg ctxt result = |
103 let |
102 let |
209 |
208 |
210 (* tactic *) |
209 (* tactic *) |
211 fun eqvt_tac ctxt config = |
210 fun eqvt_tac ctxt config = |
212 CONVERSION (eqvt_conv ctxt config) |
211 CONVERSION (eqvt_conv ctxt config) |
213 |
212 |
214 (* setup of the configuration value *) |
|
215 val setup = |
|
216 trace_eqvt_setup |
|
217 |
|
218 |
213 |
219 (** methods **) |
214 (** methods **) |
220 fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan |
215 fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan |
221 |
216 |
222 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- |
217 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- |