equal
deleted
inserted
replaced
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 |