src/Pure/Isar/attrib.ML
changeset 42669 04dfffda5671
parent 42616 92715b528e78
child 42808 30870aee8a3f
equal deleted inserted replaced
42668:b98f22593f97 42669:04dfffda5671
   439   register_config Printer.show_types_raw #>
   439   register_config Printer.show_types_raw #>
   440   register_config Printer.show_structs_raw #>
   440   register_config Printer.show_structs_raw #>
   441   register_config Printer.show_question_marks_raw #>
   441   register_config Printer.show_question_marks_raw #>
   442   register_config Syntax.ambiguity_level_raw #>
   442   register_config Syntax.ambiguity_level_raw #>
   443   register_config Syntax_Trans.eta_contract_raw #>
   443   register_config Syntax_Trans.eta_contract_raw #>
   444   register_config Name_Space.long_names_raw #>
   444   register_config Name_Space.names_long_raw #>
   445   register_config Name_Space.short_names_raw #>
   445   register_config Name_Space.names_short_raw #>
   446   register_config Name_Space.unique_names_raw #>
   446   register_config Name_Space.names_unique_raw #>
   447   register_config ML_Context.trace_raw #>
   447   register_config ML_Context.trace_raw #>
   448   register_config Proof_Context.show_abbrevs_raw #>
   448   register_config Proof_Context.show_abbrevs_raw #>
   449   register_config Goal_Display.goals_limit_raw #>
   449   register_config Goal_Display.goals_limit_raw #>
   450   register_config Goal_Display.show_main_goal_raw #>
   450   register_config Goal_Display.show_main_goal_raw #>
   451   register_config Goal_Display.show_consts_raw #>
   451   register_config Goal_Display.show_consts_raw #>