# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1320940453 0
# Node ID fc00bb412a65131a63103b754acd3e0300bf87bc
# Parent  94216a7fc1fcfba543b2ddfe0977ab1a613d9e99
tuned

diff -r 94216a7fc1fc -r fc00bb412a65 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Wed Nov 09 20:57:15 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Thu Nov 10 15:54:13 2011 +0000
@@ -35,8 +35,8 @@
 section {* Theories and Setups\label{sec:theories} *}
 
 text {*
-  Theories, as said above, are a basic layer of abstraction in
-  Isabelle. They contain definitions, syntax declarations, axioms,
+  Theories, as said above, are the most basic layer of abstraction in
+  Isabelle. They record information about definitions, syntax declarations, axioms,
   theorems and much more.  For example, if a definition is made, it
   must be stored in a theory in order to be usable later on. Similar
   with proofs: once a proof is finished, the proved theorem needs to
@@ -70,8 +70,8 @@
   for effective Isabelle programming.
 
   An important Isabelle command with theories is \isacommand{setup}. In the
-  previous chapters we used it to make, for example, a theorem attribute known
-  to Isabelle or to register a theorem under a name. What happens behind the
+  previous chapters we used it already to make a theorem attribute known
+  to Isabelle and to register a theorem under a name. What happens behind the
   scenes is that \isacommand{setup} expects a function of type @{ML_type
   "theory -> theory"}: the input theory is the current theory and the output
   the theory where the attribute has been registered or the theorem has been
@@ -124,7 +124,7 @@
   @{text "> \"BAR\" :: \"nat\""}
   \end{isabelle}
 
-  returns now a (black) constant with the type @{typ nat}, as expected.
+  now returns a (black) constant with the type @{typ nat}, as expected.
 
   In a sense, \isacommand{setup} can be seen as a transaction that
   takes the current theory @{text thy}, applies an operation, and
@@ -201,23 +201,16 @@
   contain ``short-term memory data''. The reason is that a vast number of
   functions in Isabelle depend in one way or another on contexts. Even such
   mundane operations like printing out a term make essential use of contexts.
-  For this consider the following contrived proof whose only purpose is to 
+  For this consider the following contrived proof-snippet whose only purpose is to 
   fix two variables:
-
-  \def\shadecolor{gray}
-  \begin{shaded}
-  aaa
-  \end{shaded}
-
-  \mbox{}\hspace{10mm}\begin{graybox}aa\end{graybox}
 *}
 
 lemma "True"
 proof -
   txt_raw {*\mbox{}\\[-7mm]*} 
-  ML_prf{*Variable.dest_fixes @{context}*} 
+  ML_prf {* Variable.dest_fixes @{context} *} 
   txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
-  fix x y  
+ fix x y  
   txt_raw {*\mbox{}\\[-7mm]*}
   ML_prf {* Variable.dest_fixes @{context} *} 
   txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
@@ -234,7 +227,7 @@
   active at that point of the theory. Consequently, in the first call to 
   @{ML dest_fixes in Variable} this dataslot is  empty; in the second it is 
   filled with @{text x} and @{text y}. What is interesting is that contexts
-  can be stacked. For this consider the following proof fraqument
+  can be stacked. For this consider the following proof fragment
 *}
 
 lemma "True"
@@ -243,16 +236,28 @@
   { fix z w
   txt_raw {*\mbox{}\\[-7mm]*}
   ML_prf {* Variable.dest_fixes @{context} *} 
-  txt_raw {*\mbox{}\\[-7mm]*}
-  txt_raw {* \mbox{}\hspace{4mm}\mbox{} *} }
+  txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
+ }
   txt_raw {*\mbox{}\\[-7mm]*}
   ML_prf {* Variable.dest_fixes @{context} *} 
   txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
 
 text {*
+  The first time we call @{ML dest_fixes in Variable} we have four fixes variables;
+  the second time we get only the fixes variables @{text x} and @{text y} as answer. 
+  This means the curly-braces act as opening and closing statements for a context.
   The above proof corresoponds roughly to the following ML-code.
 *}
 
+ML{*val ctxt0 = @{context};
+val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;
+val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*}
+
+text {*
+  Now let us come back to the point about printing terms.
+*}
+
+
 (*
 ML{*Proof_Context.debug := true*}
 ML{*Proof_Context.verbose := true*}
diff -r 94216a7fc1fc -r fc00bb412a65 progtutorial.pdf
Binary file progtutorial.pdf has changed