--- a/ProgTutorial/Advanced.thy	Mon Nov 14 20:30:46 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Wed Nov 16 13:23:27 2011 +0000
@@ -416,14 +416,14 @@
 
   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 @{ML_struct Variable} can be used to transfer
+  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). Note that
-  the variable @{text P} stays a free variable, since it not fixed in
+  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
@@ -433,8 +433,9 @@
   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} in order to turn an arbitray term,
-  in our case @{term "P x y z x y z"}, into a theorem.
+  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
@@ -447,9 +448,56 @@
 end"
   "?P ?x ?y ?z ?x ?y ?z"}
 
-  The result is that all variables are schematic. The great point about
-  contexts is that exporting is not just concerned with variables, but
-  also assumptions. 
+  Since we fixed all variables in @{text ctxt1}, in result all of them 
+  are schematic. The great point is that exporting between contexts is 
+  not just concerned with variables, but also 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]"}
 *}