--- 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