--- a/ProgTutorial/Tactical.thy	Wed Jun 02 07:19:58 2010 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Jun 02 08:54:50 2010 +0200
@@ -106,6 +106,8 @@
 
   because then the theorems are fixed statically at compile-time.
 
+  \index{tactic@ {\tt\slshape{}tactic}}
+  \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}}
   During the development of automatic proof procedures, you will often find it
   necessary to test a tactic on examples. This can be conveniently done with
   the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
@@ -130,7 +132,9 @@
 text {*
   By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 
   user-level of Isabelle the tactic @{ML foo_tac} or 
-  any other function that returns a tactic.
+  any other function that returns a tactic. There are some goal transformation
+  that are performed by @{text "tactic"}. They can be avoided by using 
+  @{text "raw_tactic"} instead.
 
   The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
   together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}