equal
deleted
inserted
replaced
62 "dynamic case analysis on sets"; |
62 "dynamic case analysis on sets"; |
63 |
63 |
64 |
64 |
65 (* outer syntax *) |
65 (* outer syntax *) |
66 |
66 |
67 local structure P = OuterParse and K = OuterKeyword in |
|
68 |
|
69 val _ = |
67 val _ = |
70 OuterSyntax.command "inductive_cases" |
68 Outer_Syntax.command "inductive_cases" |
71 "create simplified instances of elimination rules (improper)" K.thy_script |
69 "create simplified instances of elimination rules (improper)" Keyword.thy_script |
72 (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop) |
70 (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop) |
73 >> (Toplevel.theory o inductive_cases)); |
71 >> (Toplevel.theory o inductive_cases)); |
74 |
72 |
75 end; |
73 end; |
76 |
74 |
77 end; |
|
78 |
|