513 register_config Syntax.ambiguity_limit_raw #> |
513 register_config Syntax.ambiguity_limit_raw #> |
514 register_config Syntax_Trans.eta_contract_raw #> |
514 register_config Syntax_Trans.eta_contract_raw #> |
515 register_config Name_Space.names_long_raw #> |
515 register_config Name_Space.names_long_raw #> |
516 register_config Name_Space.names_short_raw #> |
516 register_config Name_Space.names_short_raw #> |
517 register_config Name_Space.names_unique_raw #> |
517 register_config Name_Space.names_unique_raw #> |
|
518 register_config ML_Print_Depth.print_depth_raw #> |
518 register_config ML_Options.source_trace_raw #> |
519 register_config ML_Options.source_trace_raw #> |
519 register_config ML_Options.exception_trace_raw #> |
520 register_config ML_Options.exception_trace_raw #> |
520 register_config ML_Options.exception_debugger_raw #> |
521 register_config ML_Options.exception_debugger_raw #> |
521 register_config ML_Options.debugger_raw #> |
522 register_config ML_Options.debugger_raw #> |
522 register_config ML_Options.print_depth_raw #> |
|
523 register_config Proof_Context.show_abbrevs_raw #> |
523 register_config Proof_Context.show_abbrevs_raw #> |
524 register_config Goal_Display.goals_limit_raw #> |
524 register_config Goal_Display.goals_limit_raw #> |
525 register_config Goal_Display.show_main_goal_raw #> |
525 register_config Goal_Display.show_main_goal_raw #> |
526 register_config Thm.show_consts_raw #> |
526 register_config Thm.show_consts_raw #> |
527 register_config Thm.show_hyps_raw #> |
527 register_config Thm.show_hyps_raw #> |