equal
deleted
inserted
replaced
34 val del = Thm.declaration_attribute (Data.map o Thm.del_thm); |
34 val del = Thm.declaration_attribute (Data.map o Thm.del_thm); |
35 |
35 |
36 val setup = |
36 val setup = |
37 Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)]; |
37 Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)]; |
38 |
38 |
39 val _ = OuterSyntax.add_parsers |
39 val _ = |
40 [OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description) |
40 OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description) |
41 OuterKeyword.diag |
41 OuterKeyword.diag |
42 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
42 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
43 Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)))]; |
43 Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of))); |
44 |
44 |
45 end; |
45 end; |