equal
deleted
inserted
replaced
20 |
20 |
21 val eqvt_conv: Proof.context -> eqvt_config -> conv |
21 val eqvt_conv: Proof.context -> eqvt_config -> conv |
22 val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm |
22 val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm |
23 val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic |
23 val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic |
24 |
24 |
25 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
25 val perm_simp_meth: thm list * string list -> Proof.context -> Proof.method |
26 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
26 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Proof.method |
27 val args_parser: (thm list * string list) context_parser |
27 val args_parser: (thm list * string list) context_parser |
28 |
28 |
29 val trace_eqvt: bool Config.T |
29 val trace_eqvt: bool Config.T |
30 end; |
30 end; |
31 |
31 |
217 |
217 |
218 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- |
218 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- |
219 Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; |
219 Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; |
220 |
220 |
221 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
221 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
222 (Scan.repeat (Args.const true))) [] |
222 (Scan.repeat (Args.const {proper = true, strict = true}))) [] |
223 |
223 |
224 val args_parser = add_thms_parser -- exclude_consts_parser |
224 val args_parser = add_thms_parser -- exclude_consts_parser |
225 |
225 |
226 fun perm_simp_meth (thms, consts) ctxt = |
226 fun perm_simp_meth (thms, consts) ctxt = |
227 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts))) |
227 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts))) |
228 |
228 |
229 fun perm_strict_simp_meth (thms, consts) ctxt = |
229 fun perm_strict_simp_meth (thms, consts) ctxt = |