--- a/ProgTutorial/FirstSteps.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -852,7 +852,7 @@
   \end{readmore}
 *}
 
-section {* Constructing Terms Manually\label{sec:terms_types_manually} *} 
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
 
 text {*
   While antiquotations are very convenient for constructing terms, they can
@@ -904,18 +904,23 @@
 
 @{ML_response_fake [display,gray]
 "let
-  val t = @{term \"P::nat\"}
+  val trm = @{term \"P::nat\"}
   val args = [@{term \"True\"}, @{term \"False\"}]
 in
-  list_comb (t, args)
+  list_comb (trm, args)
 end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 
   Another handy function is @{ML [index] lambda}, which abstracts a variable 
   in a term. For example
-  
+
   @{ML_response_fake [display,gray]
-  "lambda @{term \"x::nat\"} @{term \"(P::nat \<Rightarrow> bool) x\"}"
+"let
+  val x_nat = @{term \"x::nat\"}
+  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+in
+  lambda x_nat trm
+end"
   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
   In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
@@ -926,10 +931,15 @@
   as in
 
   @{ML_response_fake [display,gray]
-  "lambda @{term \"x::nat\"} @{term \"(P::bool \<Rightarrow> bool) x\"}"
-  "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Free (\"x\", \"bool\"))"}
-
-  then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted. 
+"let
+  val x_int = @{term \"x::int\"}
+  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+in
+  lambda x_int trm
+end"
+  "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
+
+  then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 
   This is a fundamental principle
   of Church-style typing, where variables with the same name still differ, if they 
   have different type.
@@ -943,7 +953,7 @@
 "let
   val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
   val s2 = (@{term \"x::nat\"}, @{term \"True\"})
-  val trm =  @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
+  val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
 in
   subst_free [s1, s2] trm
 end"
@@ -967,8 +977,11 @@
   arguments. For example
 
 @{ML_response_fake [gray,display]
-  "writeln (Syntax.string_of_term @{context}
-   (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
+"let
+  val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
+in
+  writeln (Syntax.string_of_term @{context} eq)
+end"
   "True = False"}
 *}
 
@@ -977,14 +990,11 @@
   Most of the HOL-specific operations on terms and types are defined 
   in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
-*}
-
-section {* Constants *}
-
-text {*
-  There are a few subtle issues with constants. They usually crop up when
-  pattern matching terms or types, or when constructing them. While it is perfectly ok
-  to write the function @{text is_true} as follows
+
+  When constructing terms manually, there are a few subtle issues with
+  constants. They usually crop up when pattern matching terms or types, or
+  when constructing them. While it is perfectly ok to write the function
+  @{text is_true} as follows
 *}
 
 ML{*fun is_true @{term True} = true
@@ -1108,11 +1118,7 @@
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
   functions about signatures in @{ML_file "Pure/sign.ML"}.
   \end{readmore}
-*}
-
-section {* Constructing Types Manually *}
-
-text {*
+
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
   when defining constants. For example the function returning a function 
@@ -1166,12 +1172,12 @@
   call them as follows
 
   @{ML_response [gray,display]
-  "Term.add_tfrees @{term \"(a,b)\"} []"
+  "Term.add_tfrees @{term \"(a, b)\"} []"
   "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
 
   The reason for this definition is that @{ML add_tfrees in Term} can
   be easily folded over a list of terms. Similarly for all functions
-  named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
+  named @{text "add_*"} in @{ML_file "Pure/term.ML"}.
 
 *}
 
@@ -2252,4 +2258,6 @@
 
 ML {*Datatype.get_info @{theory} "List.list"*}
 
+section {* Name Space(TBD) *}
+
 end

--- a/ProgTutorial/Package/Ind_Code.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -598,7 +598,8 @@
   The problem with @{ML SUBPROOF}, however, is that it always expects us to 
   completely discharge the goal (see Section~\ref{sec:simpletacs}). This is 
   a bit inconvenient for our gradual explanation of the proof here. Therefore
-  we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF} 
+  we use first the function @{ML [index] FOCUS in Subgoal}, which does s
+  ame as @{ML SUBPROOF} 
   but does not require us to completely discharge the goal. 
 *}
 (*<*)oops(*>*)
@@ -630,13 +631,13 @@
   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
   from @{text "params"} and @{text "prems"}, respectively. To better see what is
   going in our example, we will print out these values using the printing
-  function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will
+  function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will
   supply us the @{text "params"} and @{text "prems"} as lists, we can 
   separate them using the function @{ML [index] chop}. 
 *}
 
 ML %linenosgray{*fun chop_test_tac preds rules =
-  FOCUS (fn {params, prems, context, ...} =>
+  Subgoal.FOCUS (fn {params, prems, context, ...} =>
   let
     val cparams = map snd params
     val (params1, params2) = chop (length cparams - length preds) cparams
@@ -704,7 +705,7 @@
 *}
 
 ML %linenosgray{*fun apply_prem_tac i preds rules =
-  FOCUS (fn {params, prems, context, ...} =>
+  Subgoal.FOCUS (fn {params, prems, context, ...} =>
   let
     val cparams = map snd params
     val (params1, params2) = chop (length cparams - length preds) cparams
@@ -788,7 +789,7 @@
   end) *}
 
 text {*
-  Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore. 
+  Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. 
   The full proof of the introduction rule is as follows:
 *}
 

--- a/ProgTutorial/Parsing.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -625,7 +625,7 @@
 text {*
   There is usually no need to write your own parser for parsing inner syntax, that is 
   for terms and  types: you can just call the predefined parsers. Terms can 
-  be parsed using the function @{ML OuterParse.term}. For example:
+  be parsed using the function @{ML [index] term in OuterParse}. For example:
 
 @{ML_response [display,gray]
 "let 
@@ -635,10 +635,10 @@
 end"
 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
 
-  The function @{ML OuterParse.prop} is similar, except that it gives a different
+  The function @{ML [index] prop in OuterParse} is similar, except that it gives a different
   error message, when parsing fails. As you can see, the parser not just returns 
   the parsed string, but also some encoded information. You can decode the
-  information with the function @{ML YXML.parse}. For example
+  information with the function @{ML [index] parse in YXML}. For example
 
   @{ML_response [display,gray]
   "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""

--- a/ProgTutorial/Tactical.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -525,8 +525,8 @@
   Often proofs on the ML-level involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   shown so far is very unwieldy and brittle. Some convenience and
-  safety is provided by the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}. 
-  These tactics fix the parameters 
+  safety is provided by the functions @{ML [index] FOCUS in Subgoal} and 
+  @{ML [index] SUBPROOF}. These tactics fix the parameters 
   and bind the various components of a goal state to a record. 
   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   takes a record and just prints out the content of this record (using the 
@@ -547,7 +547,7 @@
   val string_of_asms = string_of_cterms context asms
   val string_of_concl = string_of_cterm context concl
   val string_of_prems = string_of_thms_no_vars context prems   
-  val string_of_schms = string_of_cterms context (snd schematics)    
+  val string_of_schms = string_of_cterms context (map fst (snd schematics))    
  
   val _ = (writeln ("params: " ^ string_of_params);
            writeln ("schematics: " ^ string_of_schms);
@@ -557,17 +557,19 @@
 in
   all_tac 
 end*}
+
 text_raw{*
 \end{isabelle}
 \end{minipage}
 \caption{A function that prints out the various parameters provided by 
- @{ML FOCUS} and @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
-  extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
+ @{ML FOCUS in Subgoal} and @{ML SUBPROOF}. It uses the functions defined 
+  in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s 
+  and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
 
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
-apply(tactic {* FOCUS foc_tac @{context} 1 *})
+apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 
 txt {*
   The tactic produces the following printout:
@@ -582,6 +584,8 @@
   \end{tabular}
   \end{quote}
 
+  (FIXME: find out how nowadays the schmetics are handled)
+
   Notice in the actual output the brown colour of the variables @{term x} and 
   @{term y}. Although they are parameters in the original goal, they are fixed inside
   the subproof. By convention these fixed variables are printed in brown colour.
@@ -593,7 +597,7 @@
 *}
 
 apply(rule impI)
-apply(tactic {* FOCUS foc_tac @{context} 1 *})
+apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 
 txt {*
   then the tactic prints out: 
@@ -613,9 +617,9 @@
 text {*
   Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
 
-  The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former
+  The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} is that the former
   expects that the goal is solved completely, which the latter does not.  One
-  convenience of both @{ML FOCUS} and @{ML SUBPROOF} is that we can apply the
+  convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we can apply the
   assumptions using the usual tactics, because the parameter @{text prems}
   contains them as theorems. With this you can easily implement a tactic that
   behaves almost like @{ML atac}:
@@ -657,13 +661,14 @@
 
 text {*
   \begin{readmore}
-  The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in 
+  The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in 
   @{ML_file "Pure/subgoal.ML"} and also described in 
   \isccite{sec:results}. 
   \end{readmore}
 
-  Similar but less powerful functions than @{ML FOCUS} are @{ML [index] SUBGOAL}
-  and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
+  Similar but less powerful functions than @{ML FOCUS in Subgoal} are 
+  @{ML [index] SUBGOAL} and @{ML [index] CSUBGOAL}. They allow you to 
+  inspect a given subgoal (the former
   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   cterm}). With this you can implement a tactic that applies a rule according
   to the topmost logic connective in the subgoal (to illustrate this we only
@@ -1053,12 +1058,11 @@
   will solve all trivial subgoals involving @{term True} or @{term "False"}.
 
   (FIXME: say something about @{ML [index] COND} and COND')
-
-  (FIXME: say something about @{ML [index] FOCUS})
   
   \begin{readmore}
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
+  The function @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in @{ML_file "Pure/subgoal.ML"}
   \end{readmore}
 
 *}

Binary file progtutorial.pdf has changed