--- a/ProgTutorial/Tactical.thy	Wed Dec 02 03:46:32 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Dec 02 17:06:41 2009 +0100
@@ -2311,7 +2311,8 @@
 end*}
 
 text {*
-  The function @{ML bottom_conv in More_Conv} traverses first the the term and
+  If we regard terms as trees with variables and constants on the top, then 
+  @{ML bottom_conv in More_Conv} traverses first the the term and
   on the ``way down'' applies the conversion, whereas @{ML top_conv in
   More_Conv} applies the conversion on the ``way up''. To see the difference, 
   assume the following two meta-equations.