diff -r 80b56d9b322f -r 9cf3bc448210 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -331,8 +331,30 @@
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic
-  variables. If you use the predefined tactics, which we describe in the next
-  section, this will always be the case.
+  variables. The instantiations of schematic variables can even be observed 
+  on the user level. For this consider the following definition and proof.
+*}
+
+definition 
+  EQ_TRUE 
+where
+  "EQ_TRUE X \<equiv> (X = True)"
+
+lemma test: 
+  shows "EQ_TRUE ?X"
+  unfolding EQ_TRUE_def
+  by (rule refl)
+
+text {*
+  Although Isabelle issues a warning message when stating goals involving 
+  meta-variables, it is possible to prove this theorem. The reason for the warning 
+  message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might 
+  expect, but @{thm test}:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{thm [source] test}\\
+  @{text ">"}~@{thm test}
+  \end{isabelle}
  
   \begin{readmore}
   For more information about the internals of goals see \isccite{sec:tactical-goals}.