--- a/ProgTutorial/Helper/Command/Command.thy	Sat Apr 24 22:55:50 2010 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Mon Apr 26 05:20:01 2010 +0200
@@ -29,7 +29,7 @@
      let
        val prop = Syntax.read_prop lthy str
      in
-       Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
+       Proof.theorem NONE (K I) [[(prop,[])]] lthy
      end;
    val prove_prop_parser = OuterParse.prop >> prove_prop
    val kind = OuterKeyword.thy_goal
@@ -51,7 +51,7 @@
    let
      val trm = ML_Context.evaluate lthy true ("r", r) txt
    in
-     Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
+     Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
    end
 
    val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source

--- a/ProgTutorial/Parsing.thy	Sat Apr 24 22:55:50 2010 +0200
+++ b/ProgTutorial/Parsing.thy	Mon Apr 26 05:20:01 2010 +0200
@@ -1160,7 +1160,7 @@
     let
       val prop = Syntax.read_prop lthy str
     in
-      Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
+      Proof.theorem NONE (K I) [[(prop, [])]] lthy
     end
   
   val kind = OuterKeyword.thy_goal
@@ -1173,7 +1173,7 @@
   The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context as argument.  The context is necessary in order to be able to use
   @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
-  In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the
+  In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
   proposition. Its argument @{ML NONE} stands for a locale (which we chose to
   omit); the argument @{ML "(K I)"} stands for a function that determines what
   should be done with the theorem once it is proved (we chose to just forget
@@ -1211,7 +1211,7 @@
    let
      val trm = ML_Context.evaluate lthy true ("r", r) txt
    in
-     Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
+     Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
    end
 
    val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source

--- a/ProgTutorial/Tactical.thy	Sat Apr 24 22:55:50 2010 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Apr 26 05:20:01 2010 +0200
@@ -365,16 +365,15 @@
 where
   "EQ_TRUE X \<equiv> (X = True)"
 
-lemma test: 
+schematic_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}. We can test this with:
+  By using \isacommand{schematic\_lemma} it is possible to prove lemmas including
+  meta-variables on the user level. However, the proved theorem is not @{text "EQ_TRUE ?X"}, 
+  as one might expect, but @{thm test}. We can test this with:
 
   \begin{isabelle}
   \isacommand{thm}~@{thm [source] test}\\
@@ -391,6 +390,7 @@
 
 *}
 
+
 section {* Simple Tactics\label{sec:simpletacs} *}
 
 text {*
@@ -568,7 +568,7 @@
 \end{figure}
 *}
 
-lemma 
+schematic_lemma 
   shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 

Binary file progtutorial.pdf has changed