equal
deleted
inserted
replaced
260 (** Isar tactic emulations **) |
260 (** Isar tactic emulations **) |
261 |
261 |
262 local |
262 local |
263 |
263 |
264 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":"); |
264 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":"); |
265 val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm); |
265 val opt_rule = Scan.option (rule_spec |-- Attrib.thm); |
266 |
266 |
267 val varss = |
267 val varss = |
268 Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name)))); |
268 Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name)))); |
269 |
269 |
270 val inst_tac = Method.bires_inst_tac false; |
270 val inst_tac = Method.bires_inst_tac false; |