
diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/FirstSteps.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -24,6 +24,8 @@
 
 section {* Including ML-Code *}
 
+
+
 text {*
   The easiest and quickest way to include code in a theory is
   by using the \isacommand{ML} command. For example\smallskip
@@ -37,18 +39,8 @@
   Expressions inside \isacommand{ML} commands are immediately evaluated,
   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
   your Isabelle environment. The code inside the \isacommand{ML} command 
-  can also contain value and function bindings. However on such \isacommand{ML}
-  commands the undo operation behaves slightly counter-intuitive, because 
-  if you define\smallskip
- 
-\isa{\isacommand{ML}
-\isacharverbatimopen\isanewline
-\hspace{5mm}@{ML_text "val foo = true"}\isanewline
-\isacharverbatimclose\isanewline
-@{ML_text "> true"}\smallskip}
-
-  then Isabelle's undo operation has no effect on the definition of 
-  @{ML_text "foo"}. Note that from now on we will drop the 
+  can also contain value and function bindings, and even those can be
+  undone when the proof script is retracted. From now on we will drop the 
   \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
   we show code and its response.
 
@@ -78,7 +70,7 @@
 
   @{ML [display] "warning \"any string\""}
 
-  will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle.
+  will print out @{ML_text [quotes] "any string"} inside the response buffer of Isabelle.
   If you develop under PolyML, then there is a convenient, though again 
   ``quick-and-dirty'', method for converting values into strings, 
   for example: 
@@ -101,7 +93,7 @@
   amounts of trace output. This rediretion can be achieved using the code
 *}
 
-ML {*
+ML{* 
 val strip_specials =
 let
   fun strip ("\^A" :: _ :: cs) = strip cs
@@ -113,7 +105,7 @@
  Output.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
      TextIO.output (stream, "\n");
-     TextIO.flushOut stream));
+     TextIO.flushOut stream)); 
 *}
 
 text {*
@@ -163,8 +155,8 @@
   @{ML [display] "@{thm allI}"}
   @{ML [display] "@{simpset}"}
 
-  While antiquotations have many uses, they were introduced to avoid explicit
-  bindings for theorems such as
+  While antiquotations have many applications, they were originally introduced to 
+  avoid explicit bindings for theorems such as
 *}
 
 ML {*
@@ -172,14 +164,12 @@
 *}
 
 text {*
-  These bindings were difficult to maintain and also could be overwritten
-  by bindings introduced by the user. This had the potential to break
-  definitional packages. This additional layer of maintenance complexity
-  can be avoided by using antiquotations, since they are ``linked'' statically
-  at compile time.  In the course of this introduction, we will learn more about 
-  these antiquotations: they greatly simplify Isabelle programming since one
-  can directly access all kinds of logical elements from ML.
-
+  These bindings were difficult to maintain and also could be accidentally overwritten
+  by the user. This usually broke definitional packages. Antiquotations solve this
+  problem, since they are ``linked'' statically at compile time.  In the course of this 
+  introduction, we will learn more about these antiquotations: they greatly simplify 
+  Isabelle programming since one can directly access all kinds of logical elements 
+  from ML.
 *}
 
 section {* Terms and Types *}
@@ -208,10 +198,8 @@
 
   Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user level, because the layers of
-  parsing/type checking/pretty printing can be quite elaborate. 
-*}
+  parsing/type-checking/pretty printing can be quite elaborate. 
 
-text {*
   \begin{exercise}
   Look at the internal term representation of the following terms, and
   find out why they are represented like this.
@@ -246,24 +234,14 @@
   which does not. 
 
   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
-  
-  *}
-
-
-text {*
 
   @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
-  (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
-  internal representation. Is there a reason for this, that needs to be explained 
-  here?)
-
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
   definition and many useful operations can be found in @{ML_file "Pure/type.ML"}.
   \end{readmore}
-
-  *}
+*}
 
 
 section {* Constructing Terms and Types Manually *} 
@@ -271,7 +249,7 @@
 text {*
 
   While antiquotations are very convenient for constructing terms and types, 
-  they can only construct fixed terms. Unfortunately, one often needs to construct them 
+  they can only construct fixed terms. Unfortunately, one often needs to construct terms
   dynamically. For example, a function that returns the implication 
   @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
   as arguments can only be written as
@@ -289,7 +267,8 @@
 text {*
 
   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
-  @{term "tau"} into an antiquotation. For example the following does not work.
+  @{term "tau"} into an antiquotation. For example the following does not work as
+  expected.
 *}
 
 ML {*
@@ -350,6 +329,8 @@
 
 section {* Type Checking *}
 
+ML {* cterm_of @{theory} @{term "a + b = c"} *}
+
 text {* 
   
   We can freely construct and manipulate terms, since they are just
@@ -364,11 +345,15 @@
 
   Type checking is always relative to a theory context. For now we can use
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
-  For example we can write:
+  For example we can write
+
+  @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+
+  or use the antiquotation
 
   @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 
-  and 
+  A slightly more elaborate example is
 
 @{ML_response_fake [display] 
 "let




