455 register_config Syntax.ambiguity_limit_raw #> |
455 register_config Syntax.ambiguity_limit_raw #> |
456 register_config Syntax_Trans.eta_contract_raw #> |
456 register_config Syntax_Trans.eta_contract_raw #> |
457 register_config Name_Space.names_long_raw #> |
457 register_config Name_Space.names_long_raw #> |
458 register_config Name_Space.names_short_raw #> |
458 register_config Name_Space.names_short_raw #> |
459 register_config Name_Space.names_unique_raw #> |
459 register_config Name_Space.names_unique_raw #> |
460 register_config ML_Context.source_trace_raw #> |
460 register_config ML_Options.source_trace_raw #> |
461 register_config ML_Compiler.print_depth_raw #> |
461 register_config ML_Options.exception_trace_raw #> |
462 register_config Runtime.exception_trace_raw #> |
462 register_config ML_Options.print_depth_raw #> |
463 register_config Proof_Context.show_abbrevs_raw #> |
463 register_config Proof_Context.show_abbrevs_raw #> |
464 register_config Goal_Display.goals_limit_raw #> |
464 register_config Goal_Display.goals_limit_raw #> |
465 register_config Goal_Display.show_main_goal_raw #> |
465 register_config Goal_Display.show_main_goal_raw #> |
466 register_config Goal_Display.show_consts_raw #> |
466 register_config Goal_Display.show_consts_raw #> |
467 register_config Display.show_hyps_raw #> |
467 register_config Display.show_hyps_raw #> |