equal
deleted
inserted
replaced
5 |
5 |
6 signature NOMINAL_PERMEQ = |
6 signature NOMINAL_PERMEQ = |
7 sig |
7 sig |
8 val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
8 val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
9 val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
9 val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
|
10 |
|
11 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
|
12 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
|
13 val args_parser: (thm list * string list) context_parser |
|
14 |
10 val trace_eqvt: bool Config.T |
15 val trace_eqvt: bool Config.T |
11 val setup: theory -> theory |
16 val setup: theory -> theory |
12 end; |
17 end; |
13 |
18 |
14 (* |
19 (* |
155 |
160 |
156 (* setup of the configuration value *) |
161 (* setup of the configuration value *) |
157 val setup = |
162 val setup = |
158 trace_eqvt_setup |
163 trace_eqvt_setup |
159 |
164 |
|
165 |
|
166 (** methods **) |
|
167 |
|
168 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
|
169 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
170 (Scan.repeat (Args.const true))) [] |
|
171 |
|
172 val args_parser = |
|
173 add_thms_parser -- exclude_consts_parser || |
|
174 exclude_consts_parser -- add_thms_parser >> swap |
|
175 |
|
176 fun perm_simp_meth (thms, consts) ctxt = |
|
177 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) |
|
178 |
|
179 fun perm_strict_simp_meth (thms, consts) ctxt = |
|
180 SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) |
|
181 |
160 end; (* structure *) |
182 end; (* structure *) |