src/Pure/Isar/isar_syn.ML
changeset 32804 ca430e6aee1c
parent 31869 01fed718958c
child 32805 9b535493ac8d
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Sep 27 11:50:27 2009 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 29 22:15:54 2009 +0200
     1.3 @@ -800,10 +800,15 @@
     1.4        o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
     1.8 +  OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag
     1.9      (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
    1.10  
    1.11  val _ =
    1.12 +  OuterSyntax.improper_command "print_interps"
    1.13 +    "print interpretations of locale for this theory" K.diag
    1.14 +    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
    1.15 +
    1.16 +val _ =
    1.17    OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
    1.18      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
    1.19