equal
deleted
inserted
replaced
579 val print_antiquotationsP = |
579 val print_antiquotationsP = |
580 OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag |
580 OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag |
581 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); |
581 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); |
582 |
582 |
583 val thms_containingP = |
583 val thms_containingP = |
584 OuterSyntax.improper_command "thms_containing" "print theorems containing certain constants" |
584 OuterSyntax.improper_command "thms_containing" |
|
585 "print facts containing certain constants or variables" |
585 K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing)); |
586 K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing)); |
586 |
587 |
587 val thm_depsP = |
588 val thm_depsP = |
588 OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" |
589 OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" |
589 K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); |
590 K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); |