--- a/ProgTutorial/Essential.thy	Fri Aug 13 18:52:16 2010 +0800
+++ b/ProgTutorial/Essential.thy	Sun Aug 22 22:56:52 2010 +0800
@@ -150,8 +150,8 @@
 
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
- Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
- 
+ Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+
   where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
@@ -227,7 +227,7 @@
 
   @{ML_response [display,gray]
   "@{typ \"bool\"}"
-  "Type (\"bool\", [])"}
+  "Type (\"HOL.bool\", [])"}
 
   When printing out a list-type
   
@@ -244,7 +244,7 @@
 
    @{ML_response [display,gray]
   "@{typ \"bool \<Rightarrow> nat\"}"
-  "Type (\"fun\", [Type (\"bool\", []), Type (\"Nat.nat\", [])])"}
+  "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
 
   We can restore the usual behaviour of Isabelle's pretty printer
   with the code
@@ -496,13 +496,13 @@
   for this function is
 *}
 
-ML{*fun is_all (Const ("All", _) $ _) = true
+ML{*fun is_all (Const ("HOL.All", _) $ _) = true
   | is_all _ = false*}
 
 text {* 
   because now
 
-@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 
   matches correctly (the first wildcard in the pattern matches any type and the
   second any term).
@@ -721,9 +721,9 @@
   \begin{isabelle}*}
 ML{*fun pretty_helper aux env =
   env |> Vartab.dest  
-      |> map ((fn (s1, s2) => Pretty.block [s1, Pretty.str ";=", s2]) o aux) 
-      |> Pretty.commas 
-      |> Pretty.enum "" "[" "]" 
+      |> map aux
+      |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) 
+      |> Pretty.enum "," "[" "]" 
       |> pwriteln
 
 fun pretty_tyenv ctxt tyenv =
@@ -978,7 +978,7 @@
 text {*
   Unification of abstractions is more thoroughly studied in the context of
   higher-order pattern unification and higher-order pattern matching.  A
-  \emph{\index*{pattern}} is a well-formed beta-normal term in which the arguments to
+  \emph{\index*{pattern}} is a well-formed term in which the arguments to
   every schematic variable are distinct bounds.
   In particular this excludes terms where a
   schematic variable is an argument of another one and where a schematic
@@ -1741,7 +1741,7 @@
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achieve this is by using the function @{ML_ind prove in Goal}
   in the structure @{ML_struct Goal}. For example below we use this function
-  to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?}
+  to prove the term @{term "P \<Longrightarrow> P"}.
   
   @{ML_response_fake [display,gray]
   "let
@@ -1754,12 +1754,45 @@
 
   This function takes first a context and second a list of strings. This list
   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
-  by assumption. As before this code will produce a theorem, but the theorem
-  is not yet stored in the theorem database. 
-
+  is proved (in this case only @{text "\"P\""}).  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 by assumption. 
+
+  There is also the possibility of proving multiple goals at the same time
+  using the function @{ML_ind prove_multi in Goal}. For this let us define the
+  following three helper functions.
+*}
+
+ML{*fun rep_goals i = replicate i @{prop "f x = f x"}
+fun rep_tacs i = replicate i (rtac @{thm refl})
+
+fun multi_test ctxt i =
+  Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i) 
+    (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
+
+text {*
+  With them we can now produce three theorem instances of the 
+  proposition.
+
+  @{ML_response_fake [display, gray]
+  "multi_test @{context} 3"
+  "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
+
+  However you should be careful with @{ML prove_multi in Goal} and very
+  large goals. If you increase the counter in the code above to @{text 3000}, 
+  you will notice that takes approximately ten(!) times longer than
+  using @{ML map} and @{ML prove in Goal}.
+*}
+  
+ML{*let 
+  fun test_prove ctxt thm =
+    Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
+in
+  map (test_prove @{context}) (rep_goals 3000)
+end*}
+
+text {*
   While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
   is the function @{ML_ind make_thm in Skip_Proof} in the structure 
   @{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.

--- a/ProgTutorial/Package/Ind_Code.thy	Fri Aug 13 18:52:16 2010 +0800
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Aug 22 22:56:52 2010 +0800
@@ -596,8 +596,10 @@
             Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 
 in 
   pps |> Pretty.chunks
-      |> pwriteln
+      |> Pretty.string_of
+      |> tracing
 end*}
+
 text_raw{*
 \end{isabelle}
 \end{minipage}
@@ -788,6 +790,7 @@
   of the accessible part is such a rule. 
 *}
 
+
 lemma accpartI:
 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})

--- a/ProgTutorial/Recipes/CallML.thy	Fri Aug 13 18:52:16 2010 +0800
+++ b/ProgTutorial/Recipes/CallML.thy	Sun Aug 22 22:56:52 2010 +0800
@@ -72,7 +72,7 @@
   @{text 4} is not prime: 
 *}
 
-lemma "\<not> prime(4::nat)"
+lemma "\<not> prime (4::nat)"
   apply(rule factor_non_prime)
   apply eval
   done

Binary file progtutorial.pdf has changed