equal
deleted
inserted
replaced
1165 val _ = |
1165 val _ = |
1166 Outer_Syntax.local_theory @{command_spec "inductive_simps"} |
1166 Outer_Syntax.local_theory @{command_spec "inductive_simps"} |
1167 "create simplification rules for inductive predicates" |
1167 "create simplification rules for inductive predicates" |
1168 (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps)); |
1168 (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps)); |
1169 |
1169 |
|
1170 val _ = |
|
1171 Outer_Syntax.improper_command @{command_spec "print_inductives"} |
|
1172 "print (co)inductive definitions and monotonicity rules" |
|
1173 (Scan.succeed |
|
1174 (Toplevel.no_timing o Toplevel.unknown_context o |
|
1175 Toplevel.keep (print_inductives o Toplevel.context_of))); |
|
1176 |
1170 end; |
1177 end; |