| changeset 59936 | b8ffc3dc9e24 |
| parent 59582 | 0fbed69ff081 |
| child 60097 | d20ca79d50e4 |
--- a/src/HOL/Orderings.thy Mon Apr 06 16:30:44 2015 +0200 +++ b/src/HOL/Orderings.thy Mon Apr 06 17:06:48 2015 +0200 @@ -439,7 +439,7 @@ end; val _ = - Outer_Syntax.command @{command_spec "print_orders"} + Outer_Syntax.command @{command_keyword print_orders} "print order structures available to transitivity reasoner" (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_structures o Toplevel.context_of)));