equal
deleted
inserted
replaced
255 end; |
255 end; |
256 |
256 |
257 val _ = |
257 val _ = |
258 Outer_Syntax.command @{command_keyword print_induct_rules} |
258 Outer_Syntax.command @{command_keyword print_induct_rules} |
259 "print induction and cases rules" |
259 "print induction and cases rules" |
260 (Scan.succeed (Toplevel.unknown_context o |
260 (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of))); |
261 Toplevel.keep (print_rules o Toplevel.context_of))); |
|
262 |
261 |
263 |
262 |
264 (* access rules *) |
263 (* access rules *) |
265 |
264 |
266 val lookup_casesT = lookup_rule o #1 o #1 o get_local; |
265 val lookup_casesT = lookup_rule o #1 o #1 o get_local; |