# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256483525 -3600
# Node ID be6538c7b41da8ddeb925fb4230e23d7c73c6d26
# Parent  9cf3bc448210d1d0874833f2adc4e7af0157b859
polished

diff -r 9cf3bc448210 -r be6538c7b41d ProgTutorial/General.thy
--- 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
diff -r 9cf3bc448210 -r be6538c7b41d ProgTutorial/Package/Ind_General_Scheme.thy
--- 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"}
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}
diff -r 9cf3bc448210 -r be6538c7b41d progtutorial.pdf
Binary file progtutorial.pdf has changed