equal
deleted
inserted
replaced
54 val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop; |
54 val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop; |
55 |
55 |
56 val _ = |
56 val _ = |
57 Outer_Syntax.local_theory @{command_keyword fun_cases} |
57 Outer_Syntax.local_theory @{command_keyword fun_cases} |
58 "create simplified instances of elimination rules for function equations" |
58 "create simplified instances of elimination rules for function equations" |
59 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd)); |
59 (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo fun_cases_cmd)); |
60 |
60 |
61 end; |
61 end; |
62 |
62 |