diff -r 9cf3bc448210 -r be6538c7b41d ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sun Oct 25 15:26:03 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Sun Oct 25 16:12:05 2009 +0100
@@ -356,6 +356,8 @@
   @{text ">"}~@{thm test}
   \end{isabelle}
  
+  As can be seen, the schematic variable @{text "?X"} has been instantiated inside the proof.
+
   \begin{readmore}
   For more information about the internals of goals see \isccite{sec:tactical-goals}.
   \end{readmore}