124 "long-names" |
124 "long-names" |
125 "Show fully qualified names in Isabelle terms", |
125 "Show fully qualified names in Isabelle terms", |
126 bool_pref show_brackets |
126 bool_pref show_brackets |
127 "show-brackets" |
127 "show-brackets" |
128 "Show full bracketing in Isabelle terms", |
128 "Show full bracketing in Isabelle terms", |
129 bool_pref Proof.show_main_goal |
129 bool_pref Goal_Display.show_main_goal_default |
130 "show-main-goal" |
130 "show-main-goal" |
131 "Show main goal in proof state display", |
131 "Show main goal in proof state display", |
132 bool_pref Syntax.eta_contract |
132 bool_pref Syntax.eta_contract |
133 "eta-contract" |
133 "eta-contract" |
134 "Print terms eta-contracted"]; |
134 "Print terms eta-contracted"]; |
135 |
135 |
136 val advanced_display_preferences = |
136 val advanced_display_preferences = |
137 [nat_pref goals_limit |
137 [nat_pref Goal_Display.goals_limit_default |
138 "goals-limit" |
138 "goals-limit" |
139 "Setting for maximum number of goals printed", |
139 "Setting for maximum number of goals printed", |
140 int_pref ProofContext.prems_limit |
140 int_pref ProofContext.prems_limit |
141 "prems-limit" |
141 "prems-limit" |
142 "Setting for maximum number of premises printed", |
142 "Setting for maximum number of premises printed", |