equal
deleted
inserted
replaced
585 register_config Syntax_Trans.eta_contract_raw #> |
585 register_config Syntax_Trans.eta_contract_raw #> |
586 register_config Name_Space.names_long_raw #> |
586 register_config Name_Space.names_long_raw #> |
587 register_config Name_Space.names_short_raw #> |
587 register_config Name_Space.names_short_raw #> |
588 register_config Name_Space.names_unique_raw #> |
588 register_config Name_Space.names_unique_raw #> |
589 register_config ML_Print_Depth.print_depth_raw #> |
589 register_config ML_Print_Depth.print_depth_raw #> |
|
590 register_config ML_Env.ML_environment_raw #> |
|
591 register_config ML_Env.ML_read_global_raw #> |
|
592 register_config ML_Env.ML_write_global_raw #> |
590 register_config ML_Options.source_trace_raw #> |
593 register_config ML_Options.source_trace_raw #> |
591 register_config ML_Options.exception_trace_raw #> |
594 register_config ML_Options.exception_trace_raw #> |
592 register_config ML_Options.exception_debugger_raw #> |
595 register_config ML_Options.exception_debugger_raw #> |
593 register_config ML_Options.debugger_raw #> |
596 register_config ML_Options.debugger_raw #> |
594 register_config Proof_Context.show_abbrevs_raw #> |
597 register_config Proof_Context.show_abbrevs_raw #> |