120 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":"); |
120 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":"); |
121 val opt_rule = Scan.option (rule_spec |-- Attrib.thm); |
121 val opt_rule = Scan.option (rule_spec |-- Attrib.thm); |
122 val opt_rules = Scan.option (rule_spec |-- Attrib.thms); |
122 val opt_rules = Scan.option (rule_spec |-- Attrib.thms); |
123 |
123 |
124 val varss = |
124 val varss = |
125 Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source)))); |
125 Parse.and_list' |
|
126 (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax)))); |
126 |
127 |
127 in |
128 in |
128 |
129 |
129 val setup = |
130 val setup = |
130 Method.setup @{binding case_tac} |
131 Method.setup @{binding case_tac} |
131 (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >> |
132 (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >> |
132 (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r))) |
133 (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r))) |
133 "unstructured case analysis on types" #> |
134 "unstructured case analysis on types" #> |
134 Method.setup @{binding induct_tac} |
135 Method.setup @{binding induct_tac} |
135 (Args.goal_spec -- varss -- opt_rules >> |
136 (Args.goal_spec -- varss -- opt_rules >> |
136 (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs))) |
137 (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs))) |