equal
deleted
inserted
replaced
517 register_config Name_Space.names_long_raw #> |
517 register_config Name_Space.names_long_raw #> |
518 register_config Name_Space.names_short_raw #> |
518 register_config Name_Space.names_short_raw #> |
519 register_config Name_Space.names_unique_raw #> |
519 register_config Name_Space.names_unique_raw #> |
520 register_config ML_Options.source_trace_raw #> |
520 register_config ML_Options.source_trace_raw #> |
521 register_config ML_Options.exception_trace_raw #> |
521 register_config ML_Options.exception_trace_raw #> |
|
522 register_config ML_Options.exception_debugger_raw #> |
522 register_config ML_Options.debugger_raw #> |
523 register_config ML_Options.debugger_raw #> |
523 register_config ML_Options.print_depth_raw #> |
524 register_config ML_Options.print_depth_raw #> |
524 register_config Proof_Context.show_abbrevs_raw #> |
525 register_config Proof_Context.show_abbrevs_raw #> |
525 register_config Goal_Display.goals_limit_raw #> |
526 register_config Goal_Display.goals_limit_raw #> |
526 register_config Goal_Display.show_main_goal_raw #> |
527 register_config Goal_Display.show_main_goal_raw #> |