src/Tools/induct_tacs.ML
changeset 36960 01594f816e3a
parent 35625 9c818cab0dd0
child 40722 441260986b63
equal deleted inserted replaced
36959:f5417836dbea 36960:01594f816e3a
   114 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   114 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   115 val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   115 val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   116 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
   116 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
   117 
   117 
   118 val varss =
   118 val varss =
   119   OuterParse.and_list'
   119   Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
   120     (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
       
   121 
   120 
   122 in
   121 in
   123 
   122 
   124 val setup =
   123 val setup =
   125   Method.setup @{binding case_tac}
   124   Method.setup @{binding case_tac}