--- a/ProgTutorial/Tactical.thy	Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Thu Dec 03 14:19:13 2009 +0100
@@ -2402,7 +2402,8 @@
   goal states. This can be done with the help of the function 
   @{ML_ind CONVERSION in Tactical},
   and also some predefined conversion combinators that traverse a goal
-  state. The combinators for the goal state are: 
+  state and can selectively apply the conversion. The combinators for 
+  the goal state are: 
 
   \begin{itemize}
   \item @{ML_ind params_conv in Conv} for converting under parameters
@@ -2448,7 +2449,9 @@
 
 text {*
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
-  the conclusion according to @{ML true_conj1_conv}.
+  the conclusion according to @{ML true_conj1_conv}. If we only have one
+  conversion that should be uniformly applied to the whole goal state, we
+  can also use @{ML_ind top_conv in More_Conv}.
 
   Conversions can also be helpful for constructing meta-equality theorems.
   Such theorems are often definitions. As an example consider the following