--- a/ProgTutorial/First_Steps.thy	Mon Jun 20 00:30:32 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Mon Jun 20 13:59:58 2011 +0100
@@ -227,8 +227,8 @@
 
   where now even @{term Pair} is written with its type (@{term Pair} is the
   term-constructor for products). Other configuration values that influence
-  printing of terms are @{ML_ind show_brackets in Syntax} and @{ML_ind
-  show_sorts in Syntax}.
+  printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind
+  show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}.
 *}
 
 text {*
@@ -1304,6 +1304,22 @@
 end"
   "(\"some string\", \"foo\", \"bar\")"}
 
+  A concrete example for a configuration value is 
+  @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
+  in the simplifier. This can be used as in the following proof
+*}
+
+lemma
+  shows "(False \<or> True) \<and> True"
+proof (rule conjI)
+  show "False \<or> True" using [[simp_trace = true]] by simp
+next
+  show "True" by simp
+qed
+
+text {*
+  in order to inspect how the simplifier solves the first subgoal.
+
   \begin{readmore}
   For more information about configuration values see 
   the files @{ML_file "Pure/Isar/attrib.ML"} and