src/HOL/Orderings.thy
changeset 58893 9e0ecb66d6a7
parent 58889 5b7a9633cfa8
child 59000 6eb0725503fc
equal deleted inserted replaced
58892:20aa19ecf2cc 58893:9e0ecb66d6a7
   437   in
   437   in
   438     Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
   438     Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
   439   end;
   439   end;
   440 
   440 
   441 val _ =
   441 val _ =
   442   Outer_Syntax.improper_command @{command_spec "print_orders"}
   442   Outer_Syntax.command @{command_spec "print_orders"}
   443     "print order structures available to transitivity reasoner"
   443     "print order structures available to transitivity reasoner"
   444     (Scan.succeed (Toplevel.unknown_context o
   444     (Scan.succeed (Toplevel.unknown_context o
   445       Toplevel.keep (print_structures o Toplevel.context_of)));
   445       Toplevel.keep (print_structures o Toplevel.context_of)));
   446 
   446 
   447 
   447