equal
deleted
inserted
replaced
589 register_config ML_Print_Depth.print_depth_raw #> |
589 register_config ML_Print_Depth.print_depth_raw #> |
590 register_config ML_Options.source_trace_raw #> |
590 register_config ML_Options.source_trace_raw #> |
591 register_config ML_Options.exception_trace_raw #> |
591 register_config ML_Options.exception_trace_raw #> |
592 register_config ML_Options.exception_debugger_raw #> |
592 register_config ML_Options.exception_debugger_raw #> |
593 register_config ML_Options.debugger_raw #> |
593 register_config ML_Options.debugger_raw #> |
|
594 register_config Global_Theory.pending_shyps_raw #> |
594 register_config Proof_Context.show_abbrevs_raw #> |
595 register_config Proof_Context.show_abbrevs_raw #> |
595 register_config Goal_Display.goals_limit_raw #> |
596 register_config Goal_Display.goals_limit_raw #> |
596 register_config Goal_Display.show_main_goal_raw #> |
597 register_config Goal_Display.show_main_goal_raw #> |
597 register_config Thm.show_consts_raw #> |
598 register_config Thm.show_consts_raw #> |
598 register_config Thm.show_hyps_raw #> |
599 register_config Thm.show_hyps_raw #> |