--- a/CookBook/FirstSteps.thy	Tue Feb 17 02:12:19 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Feb 17 13:53:54 2009 +0000
@@ -223,6 +223,7 @@
   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
   binds the corresponding variable. However, in Isabelle the names of bound variables are 
   kept at abstractions for printing purposes, and so should be treated only as comments. 
+  Application in Isabelle is realised with the term-constructor @{ML $}.
 
   \begin{readmore}
   Terms are described in detail in \isccite{sec:terms}. Their
@@ -429,13 +430,15 @@
 
   (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
 
+  (FIXME: say something about constants and variables having types as
+  arguments and how they can be constructed with fast-type and dummT)
 *}
 
 section {* Constants *}
 
 text {*
   There are a few subtle issues with constants. They usually crop up when
-  pattern matching terms or constructing term. While it is perfectly ok
+  pattern matching terms or constructing terms. While it is perfectly ok
   to write the function @{text is_true} as follows
 *}
 
@@ -451,12 +454,12 @@
   | is_all _ = false*}
 
 text {* 
-  will not correctly match: 
+  will not correctly match the formula @{prop "\<forall>x::nat. P x"}: 
 
   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
   The problem is that the @{text "@term"}-antiquotation in the pattern 
-  fixes the type of @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
+  fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
   an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
   for this function is
 *}
@@ -469,42 +472,46 @@
 
 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 
-  matches correctly.
+  matches correctly (the wildcard in the pattern matches any type).
 
-  However there is still a problem: consider the function that attempts to 
-  pick out a @{text "Nil"}-term:
+  However there is still a problem: consider the similar function that
+  attempts to pick out a @{text "Nil"}-term:
 *}
 
 ML{*fun is_nil (Const ("Nil", _)) = true
   | is_nil _ = false *}
 
 text {* 
-  Unfortunately, also this one does not return the expected result, since
+  Unfortunately, also this function does \emph{not} work as expected, since
 
   @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
 
-  The problem is that on the ML-level the name of constants is not
-  immediately clear. If you look at
+  The problem is that on the ML-level the name of a constant is more
+  subtle as you might expect. The function @{ML is_all} worked correctly,
+  because @{term "All"} is such a fundamental constant, which can be referenced
+  by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
 
   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 
   the name of the constant depends on the theory in which the term constructor
-  @{text "Nil"} is defined and also in which datatype. Even worse, some
-  constants have an even more complex name involving type-classes. Consider 
-  for example
+  @{text "Nil"} is defined (@{text "List"}) and also in which datatype 
+  (@{text "list"}). Even worse, some constants have a name involving 
+  type-classes. Consider for example the constants for @{term "zero"} 
+  and @{term "(op *)"}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
   "(Const (\"HOL.zero_class.zero\", \<dots>), 
  Const (\"HOL.times_class.times\", \<dots>))"}
 
-  While you could always use the complete name, for example 
-  @{ML "Const (\"List.list.Nil\", @{typ \"nat list\"})"}, for referring to or
+  While you could use the complete name, for example 
+  @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
   matching against @{text "Nil"}, this would make the code rather brittle. 
   The reason is that the theory and the name of the datatype can easily change. 
-  To make the code more robust it is better to use the antiquotation 
+  To make the code more robust, it is better to use the antiquotation 
   @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
-  variable parts of the constant's name. Therefore the functions for 
-  matching against constants should be written as follows.
+  variable parts of the constant's name. Therefore a functions for 
+  matching against constants that have a polymorphic type should 
+  be written as follows.
 *}
 
 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
@@ -512,9 +519,9 @@
   | is_nil_or_all _ = false *}
 
 text {*
-  Having said this, you also frequently have to calculate what the
-  ``base''  name of a constant is. For this you can use the function 
-  @{ML Sign.base_name}. For example:
+  Note that you also frequently have to calculate what the
+  ``base''  name of a given constant is. For this you can use 
+  the function @{ML Sign.base_name}. For example:
   
   (FIXME is there an example for that statement?)
 
@@ -597,14 +604,6 @@
   (FIXME: how to add case-names to goal states)
 *}
 
-section {* Theories and Local Theories *}
-
-section {* Storing Theorems *}
-
-text {* @{ML PureThy.add_thms_dynamic} *}
-
-section {* Theorem Attributes *}
-
 section {* Printing Terms and Theorems\label{sec:printing} *}
 
 text {* 
@@ -657,6 +656,14 @@
 ML{*fun str_of_thms ctxt thms =  
   commas (map (str_of_thm ctxt) thms)*}
 
+section {* Theorem Attributes *}
+
+section {* Theories and Local Theories *}
+
+section {* Storing Theorems *}
+
+text {* @{ML PureThy.add_thms_dynamic} *}
+
 
 section {* Combinators\label{sec:combinators} *}