--- a/ProgTutorial/General.thy	Sun Oct 25 15:26:03 2009 +0100
+++ b/ProgTutorial/General.thy	Sun Oct 25 16:12:05 2009 +0100
@@ -1093,7 +1093,7 @@
   "?P \<Longrightarrow> ?P"}
 
   This function takes first a context and second a list of strings. This list
-  specifies which variables should be turned into meta-variables once the term
+  specifies which variables should be turned into schematic variables once the term
   is proved.  The fourth argument is the term to be proved. The fifth is a
   corresponding proof given in form of a tactic (we explain tactics in
   Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem

--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Sun Oct 25 15:26:03 2009 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Sun Oct 25 16:12:05 2009 +0100
@@ -108,10 +108,10 @@
   @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
 
   where in the @{text "rules"}-part every @{text pred} is replaced by a fresh
-  meta-variable @{text "?P"}.
+  schematic variable @{text "?P"}.
 
   In order to derive an induction principle for the predicate @{text "pred"},
-  we first transform @{text ind} into the object logic and fix the meta-variables. 
+  we first transform @{text ind} into the object logic and fix the schematic variables. 
   Hence we have to prove a formula of the form
 
   @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}

--- 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}

Binary file progtutorial.pdf has changed