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