
diff -r 007922777ff1 -r ee864694315b ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Aug 17 20:57:32 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Aug 18 01:05:56 2009 +0200
@@ -8,8 +8,8 @@
 chapter {* First Steps *}
 
 text {*
-  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
-  for Isabelle must be part of a theory. If you want to follow the code given in
+  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
+  Isabelle must be part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
 
   \begin{quote}
@@ -28,22 +28,22 @@
 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:
-
-\begin{isabelle}
-\begin{graybox}
-\isacommand{ML}~@{text "\<verbopen>"}\isanewline
-\hspace{5mm}@{ML "3 + 4"}\isanewline
-@{text "\<verbclose>"}\isanewline
-@{text "> 7"}\smallskip
-\end{graybox}
-\end{isabelle}
-
-  Like normal Isabelle scripts, \isacommand{ML}-commands can be
-  evaluated 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, for example
+  The easiest and quickest way to include code in a theory is by using the
+  \isacommand{ML}-command. For example:
+
+  \begin{isabelle}
+  \begin{graybox}
+  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
+  \hspace{5mm}@{ML "3 + 4"}\isanewline
+  @{text "\<verbclose>"}\isanewline
+  @{text "> 7"}\smallskip
+  \end{graybox}
+  \end{isabelle}
+
+  Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated 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, for example
 *}
 
 ML %gray {* 
@@ -52,16 +52,15 @@
 *}
 
 text {*
-  and even those can be undone when the proof
-  script is retracted.  As mentioned in the Introduction, we will drop the
-  \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
-  show code. The lines prefixed with @{text [quotes] ">"} are not part of the
-  code, rather they indicate what the response is when the code is evaluated.
-  There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
-  including ML-code. The first evaluates the given code, but any effect on the 
-  theory, in which the code is embedded, is suppressed. The second needs to 
-  be used if ML-code is defined 
-  inside a proof. For example
+  and even those can be undone when the proof script is retracted.  As
+  mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
+  "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
+  prefixed with @{text [quotes] ">"} are not part of the code, rather they
+  indicate what the response is when the code is evaluated.  There are also
+  the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
+  ML-code. The first evaluates the given code, but any effect on the theory,
+  in which the code is embedded, is suppressed. The second needs to be used if
+  ML-code is defined inside a proof. For example
 
   \begin{quote}
   \begin{isabelle}
@@ -72,8 +71,8 @@
   \end{isabelle}
   \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).
+  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).
 
   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 
@@ -105,44 +104,44 @@
   \end{tabular}
   \end{quote}
 
-  Note that no parentheses are given this time. Note also that the 
-  included ML-file should not contain any
-  \isacommand{use} itself. Otherwise Isabelle is unable to record all
-  file dependencies, which is a nuisance if you have to track down
-  errors.
+  Note that no parentheses are given this time. Note also that the included
+  ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
+  is unable to record all file dependencies, which is a nuisance if you have
+  to track down errors.
 *}
 
 section {* Debugging and Printing\label{sec:printing} *}
 
 text {*
-
-  During development you might find it necessary to inspect some data
-  in your code. This can be done in a ``quick-and-dirty'' fashion using 
-  the function @{ML [index] "writeln"}. For example 
+  During development you might find it necessary to inspect some data in your
+  code. This can be done in a ``quick-and-dirty'' fashion using the function
+  @{ML [index] "writeln"}. For example
 
   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 
-  will print out @{text [quotes] "any string"} inside the response buffer
-  of Isabelle.  This function expects a string as argument. If you develop under PolyML,
-  then there is a convenient, though again ``quick-and-dirty'', method for
-  converting values into strings, namely the function @{ML PolyML.makestring}:
+  will print out @{text [quotes] "any string"} inside the response buffer of
+  Isabelle.  This function expects a string as argument. If you develop under
+  PolyML, then there is a convenient, though again ``quick-and-dirty'', method
+  for converting values into strings, namely the function 
+  @{ML [index] makestring in PolyML}:
 
   @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 
 
-  However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic 
-  and not a function.
-
-  The function @{ML "writeln"} should only be used for testing purposes, because any
-  output this function generates will be overwritten as soon as an error is
-  raised. For printing anything more serious and elaborate, the
-  function @{ML [index] tracing} is more appropriate. This function writes all output into
-  a separate tracing buffer. For example:
+  However, @{ML makestring in PolyML} only works if the type of what
+  is converted is monomorphic and not a function.
+
+  The function @{ML "writeln"} should only be used for testing purposes,
+  because any output this function generates will be overwritten as soon as an
+  error is raised. For printing anything more serious and elaborate, the
+  function @{ML [index] tracing} is more appropriate. This function writes all
+  output into a separate tracing buffer. For example:
 
   @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 
-  It is also possible to redirect the ``channel'' where the string @{text "foo"} is 
-  printed to a separate file, e.g., to prevent ProofGeneral from choking on massive 
-  amounts of trace output. This redirection can be achieved with the code:
+  It is also possible to redirect the ``channel'' where the string @{text
+  "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
+  choking on massive amounts of trace output. This redirection can be achieved
+  with the code:
 *}
 
 ML{*val strip_specials =
@@ -198,7 +197,7 @@
 
 text {*
   Most often you want to inspect data of Isabelle's most basic data
-  structures, namely @{ML_type term}, @{ML_type cterm} or @{ML_type
+  structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
   thm}. Isabelle contains elaborate pretty-printing functions for printing
   them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
   are a bit unwieldy. One way to transform a term into a string is to use the
@@ -270,8 +269,8 @@
 
   In order to improve the readability of theorems we convert these schematic
   variables into free variables using the function @{ML [index] import in
-  Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from
-  Isabelle's user-level.
+  Variable}. This is similar to statements like @{text "conjI[no_vars]"} 
+  from Isabelle's user-level.
 *}
 
 ML{*fun no_vars ctxt thm =
@@ -524,9 +523,9 @@
   These two functions can be used to avoid explicit @{text "lets"} for
   intermediate values in functions that return pairs. Suppose for example you
   want to separate a list of integers into two lists according to a
-  treshold. For example if the treshold is @{ML "5"}, the list @{ML
-  "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}.  This
-  function can be implemented as
+  treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
+  should be separated to @{ML "([1,2,3,4], [6,5])"}.  This function can be
+  implemented as
 *}
 
 ML{*fun separate i [] = ([], [])
@@ -619,7 +618,7 @@
 
 text {* 
   When using combinators for writing function in waterfall fashion, it is
-  sometimes necessary to do some ``plumbing'' for fitting functions
+  sometimes necessary to do some ``plumbing'' in order to fit functions
   together. We have already seen such plumbing in the function @{ML
   apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
   list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such 




