equal
deleted
inserted
replaced
922 OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag |
922 OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag |
923 (Scan.succeed |
923 (Scan.succeed |
924 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep |
924 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep |
925 (Code.print_codesetup o Toplevel.theory_of))); |
925 (Code.print_codesetup o Toplevel.theory_of))); |
926 |
926 |
|
927 val _ = |
|
928 OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag |
|
929 (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) -- |
|
930 Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >> |
|
931 (Toplevel.no_timing oo IsarCmd.unused_thms)); |
|
932 |
927 |
933 |
928 (** system commands (for interactive mode only) **) |
934 (** system commands (for interactive mode only) **) |
929 |
935 |
930 val _ = |
936 val _ = |
931 OuterSyntax.improper_command "cd" "change current working directory" K.diag |
937 OuterSyntax.improper_command "cd" "change current working directory" K.diag |