
diff -r b4c31af6af26 -r 34b93dbf8c3c CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Thu Oct 02 05:30:46 2008 -0400
+++ b/CookBook/FirstSteps.thy	Sun Oct 05 14:29:13 2008 -0400
@@ -36,7 +36,7 @@
 *}
 
 text {*
-  The expression inside \isacommand{ML} commands is immediately evaluated,
+  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}
@@ -80,22 +80,24 @@
 
 text {*
   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
-  PolyML provides a convenient, though again ``quick-and-dirty'', method for 
-  converting arbitrary values into strings, for example: 
+  If you develop under PolyML, then there is a convenient, though again 
+  ``quick-and-dirty'', method for converting values into strings, 
+  for example: 
 *}
 
 ML {* warning (makestring 1) *}
 
 text {*
-  However this only works if the type of what is printed is monomorphic and not 
+  However this only works if the type of what is converted is monomorphic and not 
   a function.
 *}
 
 text {* 
   The funtion warning should only be used for testing purposes, because
-  any output this funtion generated will be overwritten, if an error is raised. 
-  For printing anything more serious and elaborate, the function @{ML tracing}
-  should be used. This function writes all output in a separate buffer.
+  any output this funtion generates will be overwritten, as soon as an error 
+  is raised. 
+  Therefore for printing anything more serious and elaborate, the function @{ML tracing}
+  should be used. This function writes all output into a separate buffer.
 *}
 
 ML {* tracing "foo" *}
@@ -124,7 +126,7 @@
 *}
 
 text {* 
-  Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
+  Calling @{ML_text "redirect_tracing"} with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
 *}
@@ -154,7 +156,7 @@
 *}
 
 ML {* 
-  fun current_thyname () = Context.theory_name @{theory}
+  fun not_current_thyname () = Context.theory_name @{theory}
 *}
 
 text {*
@@ -166,10 +168,9 @@
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory name.
 
-  In a similar way you can use antiquotations to refer to types and theorems:
+  In a similar way you can use antiquotations to refer to theorems:
 *}
 
-ML {* @{typ "(int * nat) list"} *}
 ML {* @{thm allI} *}
 
 text {*
@@ -238,31 +239,51 @@
 
 ML {* @{term "P x"} ; @{prop "P x"} *}
 
-text {* which inserts the coercion in the latter ase and *}
+text {* which inserts the coercion in the latter case and *}
 
 
 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
-text {* which does not. *}
+text {* 
+  which does not. 
+
+  Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
+  
+  *}
+
+ML {* @{typ "bool \<Rightarrow> nat"} *}
 
-text {* (FIXME: add something about @{text "@{typ \<dots>}"}) *}
+text {*
+  (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 *} 
 
 text {*
 
-  While antiquotations are very convenient for constructing terms (similarly types), 
+  While antiquotations are very convenient for constructing terms and types, 
   they can only construct fixed terms. Unfortunately, one often needs to construct them 
   dynamically. For example, a function that returns the implication 
-  @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments
-  can only be written as
+  @{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
 *}
 
 
 ML {*
-  fun make_imp P Q =
+  fun make_imp P Q tau =
   let
-    val x = @{term "x::nat"}
+    val x = Free ("x",tau)
   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
                                     HOLogic.mk_Trueprop (Q $ x)))
   end
@@ -270,21 +291,22 @@
 
 text {*
 
-  The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
-  an antiquotation. For example this following does not work.
+  The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
+  @{term "tau"} into an antiquotation. For example this following does not work.
 *}
 
 ML {*
-  fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
+  fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
 *}
 
 text {*
 
-  To see this apply @{text "@{term S}"} and @{text "@{term T}"} to boths functions.
-  
-  One tricky point in constructing terms by hand is to obtain the fully qualified 
-  name for constants. For example the names for @{text "zero"} or @{text "+"} are
-  more complex than one first expects, namely 
+  To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
+  to both functions. 
+
+  One tricky point in constructing terms by hand is to obtain the 
+  fully qualified name for constants. For example the names for @{text "zero"} or 
+  @{text "+"} are more complex than one first expects, namely 
 
   \begin{center}
   @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. 
@@ -295,12 +317,11 @@
   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
   Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
   expansion automatically, for example:
-
 *}
+ 
+text {*
 
-ML {* @{const_name HOL.zero}; @{const_name  plus} *}
-
-text {*
+  (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
   \begin{readmore}
   There are many functions in @{ML_file "Pure/logic.ML"} and




