# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308574798 -3600
# Node ID 00921ae66622b6721e5ad19c9faf9566f3da12c6
# Parent  e11fe0de19a51192b7b32453e3b42108d3bf26f5
more polishing

diff -r e11fe0de19a5 -r 00921ae66622 ProgTutorial/First_Steps.thy
--- 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 
diff -r e11fe0de19a5 -r 00921ae66622 progtutorial.pdf
Binary file progtutorial.pdf has changed