equal
deleted
inserted
replaced
596 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
596 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
597 (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
597 (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
598 |
598 |
599 val print_registrationsP = |
599 val print_registrationsP = |
600 OuterSyntax.improper_command "print_interps" |
600 OuterSyntax.improper_command "print_interps" |
601 "print interpretations of named locale in this theory" K.diag |
601 "print interpretations of named locale" K.diag |
602 (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); |
602 (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); |
603 |
603 |
604 val print_attributesP = |
604 val print_attributesP = |
605 OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag |
605 OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag |
606 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); |
606 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); |