# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1321302646 0
# Node ID 42bac8b169516cc2e19088d155e39c186cf38384
# Parent  7294b1b839a831c4b8d2f0147a476e5e7e63d395
more on contexts

diff -r 7294b1b839a8 -r 42bac8b16951 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Mon Nov 14 12:01:45 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Mon Nov 14 20:30:46 2011 +0000
@@ -392,8 +392,8 @@
 end"
   "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
 
-  The most useful feature of contexts is that one can export terms and theorems 
-  between them. Let us show this first in the case of terms. 
+  The most useful feature of contexts is that one can export, or transfer, 
+  terms and theorems between them. We show this first for terms. 
 
   \begin{isabelle}
   \begin{graybox}
@@ -416,7 +416,7 @@
 
   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 @{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
@@ -431,35 +431,28 @@
 
   The case of transferring theorems is even more useful. The reason is
   that the generalisation of fixed variables to schematic variables is
-  not trivial. 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 into a
-  theorem.
+  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.
 
   @{ML_response_fake [display, gray]
   "let
   val thy = @{theory}
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 
+  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"}
+  "?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. 
 *}
 
 
-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 {*
 
diff -r 7294b1b839a8 -r 42bac8b16951 progtutorial.pdf
Binary file progtutorial.pdf has changed