equal
deleted
inserted
replaced
255 pretty_rules ctxt "cases pred:" casesP] |
255 pretty_rules ctxt "cases pred:" casesP] |
256 |> Pretty.writeln_chunks |
256 |> Pretty.writeln_chunks |
257 end; |
257 end; |
258 |
258 |
259 val _ = |
259 val _ = |
260 Outer_Syntax.improper_command @{command_spec "print_induct_rules"} |
260 Outer_Syntax.command @{command_spec "print_induct_rules"} |
261 "print induction and cases rules" |
261 "print induction and cases rules" |
262 (Scan.succeed (Toplevel.unknown_context o |
262 (Scan.succeed (Toplevel.unknown_context o |
263 Toplevel.keep (print_rules o Toplevel.context_of))); |
263 Toplevel.keep (print_rules o Toplevel.context_of))); |
264 |
264 |
265 |
265 |