src/HOL/Orderings.thy
changeset 36960 01594f816e3a
parent 36635 080b755377c0
child 37767 a2b7a20d6ea3
equal deleted inserted replaced
36959:f5417836dbea 36960:01594f816e3a
   420 
   420 
   421 
   421 
   422 (** Diagnostic command **)
   422 (** Diagnostic command **)
   423 
   423 
   424 val _ =
   424 val _ =
   425   OuterSyntax.improper_command "print_orders"
   425   Outer_Syntax.improper_command "print_orders"
   426     "print order structures available to transitivity reasoner" OuterKeyword.diag
   426     "print order structures available to transitivity reasoner" Keyword.diag
   427     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   427     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   428         Toplevel.keep (print_structures o Toplevel.context_of)));
   428         Toplevel.keep (print_structures o Toplevel.context_of)));
   429 
   429 
   430 
   430 
   431 (** Setup **)
   431 (** Setup **)