equal
deleted
inserted
replaced
549 (** outer syntax **) |
549 (** outer syntax **) |
550 |
550 |
551 val print_simpsetP = |
551 val print_simpsetP = |
552 OuterSyntax.improper_command "print_simpset" "print context of Simplifier" |
552 OuterSyntax.improper_command "print_simpset" "print context of Simplifier" |
553 OuterSyntax.Keyword.diag |
553 OuterSyntax.Keyword.diag |
554 (Scan.succeed (Toplevel.keep |
554 (Scan.succeed (Toplevel.no_timing o (Toplevel.keep |
555 (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))); |
555 (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of))))); |
556 |
556 |
557 val _ = OuterSyntax.add_parsers [print_simpsetP]; |
557 val _ = OuterSyntax.add_parsers [print_simpsetP]; |
558 |
558 |
559 end; |
559 end; |
560 |
560 |