diff -r 2a69b119cdee -r e91f54791e14 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Sat Sep 06 04:32:18 2008 +0200
+++ b/CookBook/FirstSteps.thy	Tue Sep 09 14:57:23 2008 +0200
@@ -24,13 +24,23 @@
 
 chapter {* First Steps *}
 
+
 text {* 
-  Isabelle programming happens in an enhanced dialect of Standard ML,
-  which adds antiquotations containing references to the logical
-  context.
+  Isabelle programming is done Standard ML, however it often uses an 
+  antiquotation mehanism  to refer to the logical context of Isabelle.
+  The ML-code that one writes is, just like lemmas and proofs in Isabelle, 
+  part of a theory. If you want to follow the code written in this
+  chapter, we assume you are working inside the theory defined as
 
-  Just like all lemmas or proofs, all ML code that you write lives in
-  a theory, where it is embedded using the \isacommand{ML} command:
+  \begin{tabular}{@ {}l}
+  \isacommand{theory} CookBook\\
+  \isacommand{imports} Main\\
+  \isacommand{begin}\\
+  \end{tabular}
+
+
+  The easiest and quickest way to include code in a theory is
+  by using the \isacommand{ML} command. For example
 *}
 
 ML {*
@@ -38,25 +48,34 @@
 *}
 
 text {*
-  The \isacommand{ML} command takes an arbitrary ML expression, which
-  is evaluated. It can also contain value or function bindings.
+  The expression inside \isacommand{ML} commands is emmediately evaluated
+  like ``normal'' proof scripts by using the advance and retreat buttons of 
+  your Isabelle environment. The code inside the \isacommand{ML} command 
+  can also contain value- and function bindings. \marginpar{\tiny FIXME can one undo them like 
+  Isabelle lemmas/proofs - probably not}
 *}
 
 section {* Antiquotations *}
 
 text {*
   The main advantage of embedding all code in a theory is that the
-  code can contain references to entities that are defined in the
-  theory. Let us for example, print out the name of the current
-  theory:
+  code can contain references to entities that are defined on the
+  logical level of Isabelle. This is done using antiquotations.
+  For example, one can print out the name of 
+  the current theory by typing
 *}
 
 ML {* Context.theory_name @{theory} *}
 
-text {* The @{text "@{theory}"} antiquotation is substituted with the
-  current theory, whose name can then be extracted using a the
-  function @{ML "Context.theory_name"}. Note that antiquotations are
-  statically scoped. The function
+text {* 
+  where @{text "@{theory}"} is an antiquotation that is substituted with the
+  current theory (remember that we assumed we are inside the theory CookBook). 
+  The name of this theory can be extrated using a the function @{ML "Context.theory_name"}. 
+  So the code above returns the string @{ML "\"CookBook\""}.
+
+  Note that antiquotations are statically scoped, that is the value is
+  determined at ``compile-time'' not ``run-time''. For example the function
+
 *}
 
 ML {* 
@@ -64,16 +83,16 @@
 *}
 
 text {*
-  does \emph{not} return the name of the current theory. Instead, we have
-  defined the constant function that always returns the string @{ML "\"CookBook\""}, which is
-  the name of @{text "@{theory}"} at the point where the code
-  is embedded. Operationally speaking,  @{text "@{theory}"} is \emph{not}
-  replaced with code that will look up the current theory in some
-  (destructive) data structure and return it. Instead, it is really
-  replaced with the theory value.
+  does \emph{not} return the name of the current theory, if it is run in a 
+  different theory. Instead, the code above defines the constant function 
+  that always returns the string @{ML "\"CookBook\""}, no matter where the
+  function is called. Operationally speaking,  @{text "@{theory}"} is 
+  \emph{not} replaced with code that will look up the current theory in 
+  some data structure and return it. Instead, it is literally
+  replaced with the value representing the theory name.
 
-  In the course of this introduction, we will learn about more of
-  these antoquotations, which greatly simplify programming, since you
+  In the course of this introduction, we will learn more about 
+  these antoquotations: they greatly simplify Isabelle programming since one
   can directly access all kinds of logical elements from ML.
 *}
 
@@ -88,14 +107,14 @@
 
 text {*
   This shows the term @{term "(a::nat) + b = c"} in the internal
-  representation, with all gory details. Terms are just an ML
+  representation with all gory details. Terms are just an ML
   datatype, and they are defined in @{ML_file "Pure/term.ML"}.
   
-  The representation of terms uses deBruin indices: Bound variables
+  The representation of terms uses deBruin indices: bound variables
   are represented by the constructor @{ML Bound}, and the index refers to
   the number of lambdas we have to skip until we hit the lambda that
   binds the variable. The names of bound variables are kept at the
-  abstractions, but they are just comments. 
+  abstractions, but they should be treated just as comments. 
   See \ichcite{ch:logic} for more details.
 
   \begin{readmore}