--- a/ProgTutorial/Advanced.thy	Thu Nov 24 19:54:01 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -161,11 +161,12 @@
 setup %graylinenos {* fn thy => 
 let
   val tmp_thy = Theory.copy thy
-  val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)
+  val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn)
   val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
   val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
   val trm2 = Syntax.read_term_global thy "FOO baz"
-  val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)
+  val _ = pwriteln 
+    (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2))
 in
   thy
 end *}
@@ -192,6 +193,11 @@
   inference. This is relevant in situations where definitions are made later, 
   but parsing and type inference has to take already proceed as if the definitions 
   were already made.
+
+  \begin{readmore}
+  Most of the functions about theories are implemented in
+  @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}.
+  \end{readmore}
 *}
 
 section {* Contexts *}
@@ -259,7 +265,7 @@
   specified by strings. Let us come back to the point about printing terms. Consider
   printing out the term \mbox{@{text "(x, y, z, w)"}} using our function @{ML_ind pretty_term}.
   This function takes a term and a context as argument. Notice how the printing
-  of the term changes with which context is used.
+  of the term changes according to which context is used.
 
   \begin{isabelle}
   \begin{graybox}
@@ -295,20 +301,31 @@
   variables, but not @{text z} and @{text w}. In the last case all variables
   are printed as expected. The point of this example is that the context
   contains the information which variables are fixed, and designates all other
-  free variables as being alien or faulty.  While this seems like a minor
-  detail, the concept of making the context aware of fixed variables is
-  actually quite useful. For example it prevents us from fixing a variable
-  twice
+  free variables as being alien or faulty.  Therefore the highlighting. 
+  While this seems like a minor detail, the concept of making the context aware 
+  of fixed variables is actually quite useful. For example it prevents us from 
+  fixing a variable twice
 
   @{ML_response_fake [gray, display]
   "@{context}
 |> Variable.add_fixes [\"x\", \"x\"]" 
   "ERROR: Duplicate fixed variable(s): \"x\""}
 
-  More importantly it also allows us to easily create fresh free variables avoiding any 
-  clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context
-  @{text ctxt1}. Next we want to create two fresh variables of type @{typ nat}
-  as variants of the string @{text [quotes] "x"}.
+  More importantly it also allows us to easily create fresh names for
+  fixed variables.  For this you have to use the function @{ML_ind
+  variant_fixes in Variable} from the structure @{ML_struct Variable}.
+
+  @{ML_response_fake [gray, display]
+  "@{context}
+|> Variable.variant_fixes [\"y\", \"y\", \"z\"]" 
+  "([\"y\", \"ya\", \"z\"], ...)"}
+
+  Now a fresh variant for the second occurence of @{text y} is created
+  avoiding any clash. In this way we can also create fresh free variables
+  that avoid any clashes with fixed variables. In Line~3 below we fix
+  the variable @{text x} in the context @{text ctxt1}. Next we want to
+  create two fresh variables of type @{typ nat} as variants of the
+  string @{text [quotes] "x"} (Lines 6 and 7).
 
   @{ML_response_fake [display, gray, linenos]
   "let
@@ -340,10 +357,31 @@
   "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
 
   The result is @{text xb} and @{text xc} for the names of the fresh
-  variables. Note that @{ML_ind declare_term in Variable} does not fix the
-  variables; it just makes them ``known'' to the context. This is helpful when
-  parsing terms using the function @{ML_ind read_term in Syntax} from the
-  structure @{ML_struct Syntax}. Consider the following code:
+  variables, since @{text x} and @{text xa} occur in the term we declared. 
+  Note that @{ML_ind declare_term in Variable} does not fix the
+  variables; it just makes them ``known'' to the context. You can see
+  that if you print out a declared term.
+
+  \begin{isabelle}
+  \begin{graybox}
+  @{ML "let
+  val trm = @{term \"P x y z\"}
+  val ctxt1 = Variable.declare_term trm @{context}
+in
+  pwriteln (pretty_term ctxt1 trm)
+end"}\\
+  \setlength{\fboxsep}{0mm}
+  @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%
+  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}~%
+  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}~%
+  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}
+  \end{graybox}
+  \end{isabelle}
+
+  All variables are highligted, indicating that they are not
+  fixed. However, declaring a term is helpful when parsing terms using
+  the function @{ML_ind read_term in Syntax} from the structure
+  @{ML_struct Syntax}. Consider the following code:
 
   @{ML_response_fake [gray, display]
   "let
@@ -371,43 +409,116 @@
 end"
   "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
 
-  The most useful feature of contexts is that one can export, for example,
-  terms between contexts.
-*}
+  The most useful feature of contexts is that one can export, or transfer, 
+  terms and theorems between them. We show this first for terms. 
 
-ML {*
-let
+  \begin{isabelle}
+  \begin{graybox}
+  \begin{linenos}
+  @{ML "let
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
-  val foo_trm = @{term "P x y z"}
+  val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 
+  val foo_trm = @{term \"P x y z\"}
 in
   singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
-  |> pretty_term ctxt1
+  |> pretty_term ctxt0
   |> pwriteln
-end
+end"}
+  \end{linenos}
+  \setlength{\fboxsep}{0mm}
+  @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%
+  @{text "?x ?y ?z"}
+  \end{graybox}
+  \end{isabelle}
+
+  In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in
+  context @{text ctxt1}.  The function @{ML_ind export_terms in
+  Variable} from the structure @{ML_struct Variable} can be used to transfer
+  terms between contexts. Transferring means to turn all (free)
+  variables that are fixed in one context, but not in the other, into
+  schematic variables. In our example, we are transferring the term
+  @{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"},
+  which means @{term x}, @{term y} and @{term z} become schematic
+  variables (as can be seen by the leading question marks in the result). 
+  Note that the variable @{text P} stays a free variable, since it not fixed in
+  @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does
+  not know about it. Note also that in Line 6 we had to use the
+  function @{ML_ind singleton}, because the function @{ML_ind
+  export_terms in Variable} normally works over lists of terms.
+
+  The case of transferring theorems is even more useful. The reason is
+  that the generalisation of fixed variables to schematic variables is
+  not trivial if done manually. For illustration purposes we use in the 
+  following code the function @{ML_ind make_thm in Skip_Proof} from the 
+  structure @{ML_struct Skip_Proof}. This function will turn an arbitray 
+  term, in our case @{term "P x y z x y z"}, into a theorem (disregarding 
+  whether it is actually provable).
+
+  @{ML_response_fake [display, gray]
+  "let
+  val thy = @{theory}
+  val ctxt0 = @{context}
+  val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0 
+  val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
+in
+  singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
+end"
+  "?P ?x ?y ?z ?x ?y ?z"}
+
+  Since we fixed all variables in @{text ctxt1}, in the exported
+  result all of them are schematic. The great point of contexts is
+  that exporting from one to another is not just restricted to
+  variables, but also works with assumptions. For this we can use the
+  function @{ML_ind export in Assumption} from the structure
+  @{ML_struct Assumption}. Consider the following code.
+
+  @{ML_response_fake [display, gray, linenos]
+  "let
+  val ctxt0 = @{context}
+  val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
+  val eq' = Thm.symmetric eq
+in
+  Assumption.export false ctxt1 ctxt0 eq'
+end"
+  "x \<equiv> y \<Longrightarrow> y \<equiv> x"}
+  
+  The function @{ML_ind add_assumes in Assumption} from the structure
+  @{ML_struct Assumption} adds the assumption \mbox{@{text "x \<equiv> y"}}
+  to the context @{text ctxt1} (Line 3). This function expects a list
+  of @{ML_type cterm}s and returns them as theorems, together with the
+  new context in which they are ``assumed''. In Line 4 we use the
+  function @{ML_ind symmetric in Thm} from the structure @{ML_struct
+  Thm} in order to obtain the symmetric version of the assumed
+  meta-equality. Now exporting the theorem @{text "eq'"} from @{text
+  ctxt1} to @{text ctxt0} means @{term "y \<equiv> x"} will be prefixed with
+  the assumed theorem. The boolean flag in @{ML_ind export in
+  Assumption} indicates whether the assumptions should be marked with
+  the goal marker (see Section~\ref{sec:basictactics}). In normal
+  circumstances this is not necessary and so should be set to @{ML
+  false}.  The result of the export is then the theorem \mbox{@{term
+  "x \<equiv> y \<Longrightarrow> y \<equiv> x"}}.  As can be seen this is an easy way for obtaing
+  simple theorems. We will explain this in more detail in
+  Section~\ref{sec:structured}.
+
+  The function @{ML_ind export in Proof_Context} from the structure 
+  @{ML_struct Proof_Context} combines both export functions from 
+  @{ML_struct Variable} and @{ML_struct Assumption}. This can be seen
+  in the following example.
+
+  @{ML_response_fake [display, gray]
+  "let
+  val ctxt0 = @{context}
+  val ((fvs, [eq]), ctxt1) = ctxt0
+    |> Variable.add_fixes [\"x\", \"y\"]
+    ||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]
+  val eq' = Thm.symmetric eq
+in
+  Proof_Context.export ctxt1 ctxt0 [eq']
+end"
+  "[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}
 *}
 
-ML {*
-let
-  val thy = @{theory}
-  val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
-  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
-in
-  singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end
-*}
 
-ML {*
-let
-  val thy = @{theory}
-  val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
-  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
-in
-  singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end
-*}
 
 text {*
 
@@ -448,7 +559,7 @@
 oops
 *)
 
-section {* Local Theories (TBD) *}
+section {* Local Theories and Local Setups\label{sec:local} (TBD) *}
 
 text {*
   In contrast to an ordinary theory, which simply consists of a type

--- a/ProgTutorial/Essential.thy	Thu Nov 24 19:54:01 2011 +0000
+++ b/ProgTutorial/Essential.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -115,12 +115,13 @@
 end"
 "?x3, ?x1.3, x"}
 
-  When constructing terms, you are usually concerned with free variables (as
-  mentioned earlier, you cannot construct schematic variables using the
-  antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
-  however, observe the distinction. The reason is that only schematic
-  variables can be instantiated with terms when a theorem is applied. A
-  similar distinction between free and schematic variables holds for types
+  When constructing terms, you are usually concerned with free
+  variables (as mentioned earlier, you cannot construct schematic
+  variables using the built in antiquotation \mbox{@{text "@{term
+  \<dots>}"}}). If you deal with theorems, you have to, however, observe the
+  distinction. The reason is that only schematic variables can be
+  instantiated with terms when a theorem is applied. A similar
+  distinction between free and schematic variables holds for types
   (see below).
 
   \begin{readmore}
@@ -1555,8 +1556,10 @@
   While we obtained a theorem as result, this theorem is not
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced on the user level. One way to store it in the theorem database is
-  by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
-  to the section about local-setup is given here.}
+  by using the function @{ML_ind note in Local_Theory} from the structure 
+  @{ML_struct Local_Theory} (the Isabelle command
+  \isacommand{local\_setup} will be explained in more detail in 
+  Section~\ref{sec:local}).
 *}
 
 local_setup %gray {*
@@ -1598,7 +1601,7 @@
   [source] my_thm_simp} is that they can now also be referenced with the
   \isacommand{thm}-command on the user-level of Isabelle
 
-
+    
   \begin{isabelle}
   \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
   @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
@@ -2009,16 +2012,20 @@
   using @{text "@{thm \<dots>}"} produces
 
   \begin{isabelle}
+  \begin{graybox}
   @{text "@{thm style_test}"}\\
   @{text ">"}~@{thm style_test}
+  \end{graybox}
   \end{isabelle}
 
   as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} 
   we obtain
 
   \begin{isabelle}
+  \begin{graybox}
   @{text "@{thm (my_strip_allq) style_test}"}\\
   @{text ">"}~@{thm (my_strip_allq) style_test}
+  \end{graybox}
   \end{isabelle}
   
   without the leading quantifiers. We can improve this theorem style by explicitly 
@@ -2051,10 +2058,11 @@
   on the resulting term. We can now suggest, for example, two variables for
   stripping off the first two @{text \<forall>}-quantifiers.
 
-
   \begin{isabelle}
+  \begin{graybox}
   @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\
   @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
+  \end{graybox}
   \end{isabelle}
 
   Such styles allow one to print out theorems in documents formatted to 

--- a/ProgTutorial/First_Steps.thy	Thu Nov 24 19:54:01 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -76,8 +76,8 @@
   \end{isabelle}
   \end{quote}
 
-  However, both commands will only play minor roles in this tutorial (we will
-  always arrange that the ML-code is defined outside proofs).
+  However, both commands will only play minor roles in this tutorial (we most of
+  the time make sure that the ML-code is defined outside proofs).
 
   
 
@@ -211,11 +211,14 @@
 
   where now even @{term Pair} is written with its type (@{term Pair} is the
   term-constructor for products). Other configuration values that influence
-  printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind
-  show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}.
-*}
+  printing of terms include 
 
-text {*
+  \begin{itemize}
+  \item @{ML_ind show_brackets in Syntax} 
+  \item @{ML_ind show_sorts in Syntax}
+  \item @{ML_ind eta_contract in Syntax}
+  \end{itemize}
+
   A @{ML_type cterm} can be printed with the following function.
 *}
 
@@ -689,8 +692,8 @@
   pwriteln (pretty_term ctxt' one_trm);
   pwriteln (pretty_thm ctxt' one_thm)
 end"
-  "one
-one \<equiv> 1"}
+  "One
+One \<equiv> 1"}
   Recall that @{ML "|>"} is the reverse function application. Recall also that
   the related reverse function composition is @{ML "#>"}. In fact all the
   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
@@ -701,8 +704,8 @@
 *}
 
 ML{*val double =
-            (fn x => (x, x))
-        #-> (fn x => fn y => x + y)*}
+   (fn x => (x, x)) #-> 
+   (fn x => fn y => x + y)*}
 
 
 text {* 

--- a/ProgTutorial/Intro.thy	Thu Nov 24 19:54:01 2011 +0000
+++ b/ProgTutorial/Intro.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -223,7 +223,7 @@
   this. Still to keep them to a minimum, you can submit your changes first to a rather 
   sophisticated \emph{testboard}, which will perform checks of your changes against the
   Isabelle repository and against the AFP. The advantage of the testboard is
-  that the testing is performed by rather powerful machines, saving you lengthy
+  that the testing is performed by rather powerful machines saving you lengthy
   tests on, for example, your own laptop. You can see the results of the testboard 
   at 
 
@@ -241,7 +241,7 @@
 
   where the dots need to be replaced by your login name.  Note that for
   pushing changes to the testboard you need to add the option @{text "-f"},
-  which however should \emph{never} be used with the main Isabelle
+  which should \emph{never} be used with the main Isabelle
   repository. While the testboard is a great system for supporting Isabelle
   developers, its disadvantage is that it needs login permissions for the
   computers in Munich. So in order to use it, you might have to ask other

--- a/ProgTutorial/Tactical.thy	Thu Nov 24 19:54:01 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -23,7 +23,7 @@
   tactic combinators. We also describe the simplifier, simprocs and conversions.
 *}
 
-section {* Basics of Reasoning with Tactics*}
+section {* Basics of Reasoning with Tactics\label{sec:basictactics}*}
 
 text {*
   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
@@ -2543,7 +2543,7 @@
 
 section {* Declarations (TBD) *}
 
-section {* Structured Proofs (TBD) *}
+section {* Structured Proofs\label{sec:structured} (TBD) *}
 
 text {* TBD *}