equal
deleted
inserted
replaced
225 end" |
225 end" |
226 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
226 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
227 |
227 |
228 where now even @{term Pair} is written with its type (@{term Pair} is the |
228 where now even @{term Pair} is written with its type (@{term Pair} is the |
229 term-constructor for products). Other configuration values that influence |
229 term-constructor for products). Other configuration values that influence |
230 printing of terms are @{ML_ind show_brackets in Syntax} and @{ML_ind |
230 printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind |
231 show_sorts in Syntax}. |
231 show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}. |
232 *} |
232 *} |
233 |
233 |
234 text {* |
234 text {* |
235 A @{ML_type cterm} can be printed with the following function. |
235 A @{ML_type cterm} can be printed with the following function. |
236 *} |
236 *} |
1302 Config.get ctxt' sval, |
1302 Config.get ctxt' sval, |
1303 Config.get ctxt'' sval) |
1303 Config.get ctxt'' sval) |
1304 end" |
1304 end" |
1305 "(\"some string\", \"foo\", \"bar\")"} |
1305 "(\"some string\", \"foo\", \"bar\")"} |
1306 |
1306 |
|
1307 A concrete example for a configuration value is |
|
1308 @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information |
|
1309 in the simplifier. This can be used as in the following proof |
|
1310 *} |
|
1311 |
|
1312 lemma |
|
1313 shows "(False \<or> True) \<and> True" |
|
1314 proof (rule conjI) |
|
1315 show "False \<or> True" using [[simp_trace = true]] by simp |
|
1316 next |
|
1317 show "True" by simp |
|
1318 qed |
|
1319 |
|
1320 text {* |
|
1321 in order to inspect how the simplifier solves the first subgoal. |
|
1322 |
1307 \begin{readmore} |
1323 \begin{readmore} |
1308 For more information about configuration values see |
1324 For more information about configuration values see |
1309 the files @{ML_file "Pure/Isar/attrib.ML"} and |
1325 the files @{ML_file "Pure/Isar/attrib.ML"} and |
1310 @{ML_file "Pure/config.ML"}. |
1326 @{ML_file "Pure/config.ML"}. |
1311 \end{readmore} |
1327 \end{readmore} |