
diff -r 930b1308fd96 -r 8f73e80c8c6f ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sun Oct 11 16:30:59 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Oct 11 22:45:29 2009 +0200
@@ -13,7 +13,7 @@
   more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
   Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
   re-painted 18 times since its initial construction, an average of once every 
-  seven years. It takes more than a year for a team of 25 painters to paint the Tower 
+  seven years. It takes more than a year for a team of 25 painters to paint the tower 
   from top to bottom.}
   \end{flushright}
 
@@ -82,7 +82,7 @@
   \end{quote}
 
   However, both commands will only play minor roles in this tutorial (we will
-  always arrange that the ML-code is defined outside of proofs, for example).
+  always arrange that the ML-code is defined outside of proofs).
 
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a 
@@ -238,7 +238,7 @@
   "tracing (string_of_term @{context} @{term \"1::nat\"})"
   "\"1\""}
 
-  If there are more than one @{ML_type term}s to be printed, you can use the 
+  If there are more than one term to be printed, you can use the 
   function @{ML_ind  commas} to separate them.
 *} 
 
@@ -271,7 +271,7 @@
 
 text {*
   Theorems also include schematic variables, such as @{text "?P"}, 
-  @{text "?Q"} and so on. They are needed in order to able to
+  @{text "?Q"} and so on. They are needed in Isabelle in order to able to
   instantiate theorems when they are applied. For example the theorem 
   @{thm [source] conjI} shown below can be used for any (typable) 
   instantiation of @{text "?P"} and @{text "?Q"}. 
@@ -283,7 +283,7 @@
   However, in order to improve the readability when printing theorems, we
   convert these schematic variables into free variables using the function
   @{ML_ind  import in Variable}. This is similar to statements like @{text
-  "conjI[no_vars]"} from Isabelle's user-level.
+  "conjI[no_vars]"} on Isabelle's user-level.
 *}
 
 ML{*fun no_vars ctxt thm =
@@ -316,7 +316,7 @@
   Note, that when printing out several parcels of information that
   semantically belong together, like a warning message consisting for example
   of a term and a type, you should try to keep this information together in a
-  single string. Therefore do not print out information as
+  single string. Therefore do \emph{not} print out information as
 
 @{ML_response_fake [display,gray]
 "tracing \"First half,\"; 
@@ -339,8 +339,8 @@
   "cat_lines [\"foo\", \"bar\"]"
   "\"foo\\nbar\""}
 
-  Section \ref{sec:pretty} will also explain infrastructure that helps 
-  with more elaborate pretty printing. 
+  Section \ref{sec:pretty} will also explain the infrastructure of Isabelle 
+  that helps with more elaborate pretty printing. 
 *}
 
 
@@ -429,7 +429,7 @@
 text {*
   This function takes a term and a context as argument. If the term is of function
   type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
-  applied to it. For example below variables are applied to the term 
+  applied to it. For example below three variables are applied to the term 
   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 
   @{ML_response_fake [display,gray]
@@ -638,7 +638,7 @@
   plumbing is also needed in situations where a function operate over lists, 
   but one calculates only with a single element. An example is the function 
   @{ML_ind  check_terms in Syntax}, whose purpose is to type-check a list 
-  of terms.
+  of terms. Consider the code:
 
   @{ML_response_fake [display, gray]
   "let
@@ -679,7 +679,6 @@
   \end{readmore}
 
   \footnote{\bf FIXME: find a good exercise for combinators}
-
   \footnote{\bf FIXME: say something about calling conventions} 
 *}
 
@@ -687,23 +686,22 @@
 section {* ML-Antiquotations *}
 
 text {*
-  The main advantage of embedding all code in a theory is that the code can
-  contain references to entities defined on the logical level of Isabelle. By
-  this we mean definitions, theorems, terms and so on. This kind of reference
-  is realised in Isabelle with ML-antiquotations, often just called
-  antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
-  which have very different purposes and infrastructures. The first kind,
-  described in this section, are \emph{ML-antiquotations}. They are used to
-  refer to entities (like terms, types etc) from Isabelle's logic layer inside
-  ML-code. The other kind of antiquotations are \emph{document}
-  antiquotations. They are used only in the text parts of Isabelle and their
-  purpose is to print logical entities inside \LaTeX-documents. Document
-  antiquotations are part of the user level and therefore we are not
-  interested in them in this Tutorial, except in Appendix
+  Recall that code in Isabelle is always embedded in a theory.  The main
+  advantage of this is that the code can contain references to entities
+  defined on the logical level of Isabelle. By this we mean definitions,
+  theorems, terms and so on. This kind of reference is realised in Isabelle
+  with ML-antiquotations, often just called antiquotations.\footnote{There are
+  two kinds of antiquotations in Isabelle, which have very different purposes
+  and infrastructures. The first kind, described in this section, are
+  \emph{ML-antiquotations}. They are used to refer to entities (like terms,
+  types etc) from Isabelle's logic layer inside ML-code. The other kind of
+  antiquotations are \emph{document} antiquotations. They are used only in the
+  text parts of Isabelle and their purpose is to print logical entities inside
+  \LaTeX-documents. Document antiquotations are part of the user level and
+  therefore we are not interested in them in this Tutorial, except in Appendix
   \ref{rec:docantiquotations} where we show how to implement your own document
   antiquotations.}  For example, one can print out the name of the current
   theory by typing
-
   
   @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
  
@@ -835,7 +833,7 @@
   The parser in Line 2 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
   ProofContext} (Line 5); the next two lines transform the term into a string
-  so that the ML-system can understand them. An example for the usage
+  so that the ML-system can understand it. An example for the usage
   of this antiquotation is:
 
   @{ML_response_fake [display,gray]
@@ -843,6 +841,11 @@
   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 
   which shows the internal representation of the term @{text "Suc ?x"}.
+  This is different from the build-in @{text "@{term \<dots>}"}-antiquotation.
+
+  @{ML_response_fake [display,gray]
+  "@{term \"Suc (x::nat)\"}"
+  "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Free (\"x\", \"nat\")"}
 
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
@@ -1238,6 +1241,22 @@
   For more information about configuration values see 
   @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
   \end{readmore}
+ 
+*}
+
+section {* Summary *}
+
+text {*
+  This chapter describes the combinators that are used in Isabelle, as well
+  as a simple printing infrastructure for @{ML_type term}, @{ML_type cterm}
+  and @{ML_type thm}. The section on ML-antiquotations shows how to refer 
+  statically to entities from the logic level of Isabelle. Isabelle also
+  contains mechanisms for storing arbitrary data in theory and proof 
+  contexts.
+
+  This chapter also mentions two coding conventions: namely printing
+  entities belonging together as one string, and not using references
+  in any Isabelle code.
 *}
 
 




