
diff -r 84d1392186d3 -r 253ea99c1441 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Feb 25 22:13:41 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Feb 26 12:16:24 2009 +0000
@@ -141,9 +141,9 @@
    Syntax.string_of_term ctxt (term_of t)*}
 
 text {*
-  The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}.
-  If there are more than one @{ML_type cterm}s to be printed, you can use the 
-  function @{ML commas} to separate them.
+  In this example the function @{ML term_of} extracts the @{ML_type term} from
+  a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
+  printed, you can use the function @{ML commas} to separate them.
 *} 
 
 ML{*fun str_of_cterms ctxt ts =  
@@ -214,7 +214,7 @@
   common when dealing with theories (for example by adding a definition, followed by
   lemmas and so on). The reverse application allows you to read what happens in 
   a top-down manner. This kind of coding should also be familiar, 
-  if you used to Haskell's do-notation. Writing the function @{ML inc_by_five} using 
+  if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using 
   the reverse application is much clearer than writing
 *}
 
@@ -389,11 +389,11 @@
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
 
-  You can also refer to the current simpset. To illustrate this we use the
+  You can also refer to the current simpset. To illustrate this we implement the
   function that extracts the theorem names stored in a simpset.
 *}
 
-ML{*fun get_thm_names simpset =
+ML{*fun get_thm_names_from_ss simpset =
 let
   val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
 in
@@ -405,13 +405,13 @@
   information about the simpset. The rules of a simpset are stored in a
   \emph{discrimination net} (a data structure for fast indexing). From this
   net you can extract the entries using the function @{ML Net.entries}.
-  You can now use @{ML get_thm_names} to obtain all names of theorems stored
+  You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
   in the current simpset---this simpset can be referred to using the antiquotation
-  @{text "@{simpset}"}.\footnote
-  {FIXME: you cannot cleanly match against lists with ommited parts}
+  @{text "@{simpset}"}.
 
   @{ML_response_fake [display,gray] 
-"get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+  "get_thm_names_from_ss @{simpset}" 
+  "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
   \begin{readmore}
   The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
@@ -431,7 +431,7 @@
   packages. Antiquotations solve this problem, since they are ``linked''
   statically at compile-time.  However, this static linkage also limits their
   usefulness in cases where data needs to be build up dynamically. In the
-  course of this introduction, you will learn more about these antiquotations:
+  course of this chapter you will learn more about these antiquotations:
   they can simplify Isabelle programming since one can directly access all
   kinds of logical elements from th ML-level.
 
@@ -446,7 +446,7 @@
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
 "Const (\"op =\", \<dots>) $ 
-   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
   representation of this term. This internal representation corresponds to the 
@@ -456,7 +456,7 @@
   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
   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. 
+  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}
@@ -492,7 +492,7 @@
 
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
-  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+ Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
  
   where a coercion is inserted in the second component and 
 
@@ -617,7 +617,7 @@
   \end{exercise}
 
   There are a few subtle issues with constants. They usually crop up when
-  pattern matching terms or types, or constructing them. While it is perfectly ok
+  pattern matching terms or types, or when constructing them. While it is perfectly ok
   to write the function @{text is_true} as follows
 *}
 
@@ -651,7 +651,8 @@
 
 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 
-  matches correctly (the first wildcard in the pattern matches any type).
+  matches correctly (the first wildcard in the pattern matches any type and the
+  second any term).
 
   However there is still a problem: consider the similar function that
   attempts to pick out @{text "Nil"}-terms:
@@ -666,7 +667,7 @@
   @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
 
   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,
+  subtle than 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
 
@@ -732,7 +733,7 @@
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
   For example you can write:
 
-  @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+  @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"}
 
   This can also be written with an antiquotation:
 
@@ -770,15 +771,15 @@
 
   To calculate the type, this function traverses the whole term and will
   detect any typing inconsistency. For examle changing the type of the variable 
-  from @{typ "nat"} to @{typ "int"} will result in the error message: 
+  @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 
 
   @{ML_response_fake [display,gray] 
   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 
   "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
 
   Since the complete traversal might sometimes be too costly and
-  not necessary, there is also the function @{ML fastype_of}, which 
-  returns the type of a term.
+  not necessary, there is the function @{ML fastype_of}, which 
+  also returns the type of a term.
 
   @{ML_response [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
@@ -789,7 +790,7 @@
    @{ML_response [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
 
-  where no error is raised.
+  where no error is detected.
 
   Sometimes it is a bit inconvenient to construct a term with 
   complete typing annotations, especially in cases where the typing 
@@ -809,7 +810,7 @@
   Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 
   Instead of giving explicitly the type for the constant @{text "plus"} and the free 
-  variable @{text "x"}, the type-inference filled in the missing information.
+  variable @{text "x"}, the type-inference filles in the missing information.
 
   \begin{readmore}
   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
@@ -842,7 +843,6 @@
 
 @{ML_response_fake [display,gray]
 "let
-
   val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
   val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}
 
@@ -916,9 +916,9 @@
 
 text {* 
   where the function @{ML "Thm.rule_attribute"} expects a function taking a 
-  context (we ignore it in the code above) and a theorem (@{text thm}) and 
-  returns another theorem (namely @{text thm} resolved with the rule 
-  @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
+  context (which we ignore in the code above) and a theorem (@{text thm}), and 
+  returns another theorem (namely @{text thm} resolved with the lemma 
+  @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
   an attribute (of type @{ML_type "attribute"}).
 
   Before we can use the attribute, we need to set it up. This can be done
@@ -931,10 +931,11 @@
 *}
 
 text {*
-  The attribute does not expect any further arguments (like @{text "[OF \<dots>]"} that 
-  can take a list of theorems as argument). Therefore we use the function
-  @{ML Attrib.no_args}. Later on we will also consider attributes taking further
-  arguments. An example for the attribute @{text "[my_sym]"} is the proof
+  The attribute does not expect any further arguments (unlike @{text "[OF
+  \<dots>]"}, for example, which can take a list of theorems as argument). Therefore
+  we use the function @{ML Attrib.no_args}. Later on we will also consider
+  attributes taking further arguments. An example for the attribute @{text
+  "[my_sym]"} is the proof
 *} 
 
 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp




