
diff -r 609f9ef73494 -r a0edabf14457 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Sat Nov 01 15:20:36 2008 +0100
+++ b/CookBook/FirstSteps.thy	Mon Nov 24 02:51:08 2008 +0100
@@ -28,7 +28,7 @@
 
 text {*
   The easiest and quickest way to include code in a theory is
-  by using the \isacommand{ML} command. For example\smallskip
+  by using the \isacommand{ML}-command. For example\smallskip
 
 \isa{\isacommand{ML}
 \isacharverbatimopen\isanewline
@@ -36,11 +36,11 @@
 \isacharverbatimclose\isanewline
 @{ML_text "> 7"}\smallskip}
 
-  Expressions inside \isacommand{ML} commands are 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 
+  your Isabelle environment. The code inside the \isacommand{ML}-command 
   can also contain value and function bindings, and even those can be
-  undone when the proof script is retracted. From now on we will drop the 
+  undone when the proof script is retracted. In what follows we will drop the 
   \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
   we show code and its response.
 
@@ -81,10 +81,10 @@
   a function.
 
   The funtion @{ML "warning"} should only be used for testing purposes, because any
-  output this funtion generates will be overwritten, as soon as an error is
+  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 tracing buffer.
+  a separate tracing buffer. For example
 
   @{ML [display] "tracing \"foo\""}
 
@@ -119,18 +119,19 @@
 section {* 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. This is done using antiquotations.
-  For example, one can print out the name of 
-  the current theory by typing
+  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 is done using
+  antiquotations.  For example, one can print out the name of the current
+  theory by typing
+
   
   @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"}
  
   where @{text "@{theory}"} is an antiquotation that is substituted with the
-  current theory (remember that we assumed we are inside the theory CookBook). 
-  The name of this theory can be extracted using the function 
-  @{ML "Context.theory_name"}. 
+  current theory (remember that we assumed we are inside the theory 
+  @{ML_text FirstSteps}). The name of this theory can be extracted using 
+  the function @{ML "Context.theory_name"}. 
 
   Note, however, that antiquotations are statically scoped, that is the value is
   determined at ``compile-time'', not ``run-time''. For example the function
@@ -155,7 +156,7 @@
   @{ML [display] "@{thm allI}"}
   @{ML [display] "@{simpset}"}
 
-  While antiquotations have many applications, they were originally introduced to 
+  While antiquotations nowadays have many applications, they were originally introduced to 
   avoid explicit bindings for theorems such as
 *}
 
@@ -164,19 +165,21 @@
 *}
 
 text {*
-  These bindings were difficult to maintain and also could be accidentally overwritten
-  by the user. This usually broke definitional packages. Antiquotations solve this
-  problem, since they are ``linked'' statically at compile time.  In the course of this 
-  introduction, we will learn more about these antiquotations: they greatly simplify 
-  Isabelle programming since one can directly access all kinds of logical elements 
-  from ML.
+  These bindings were difficult to maintain and also could be accidentally
+  overwritten by the user. This usually broke definitional
+  packages. Antiquotations solve this problem, since they are ``linked''
+  statically at compile-time. However, that also sometimes limits there
+  applicability. In the course of this introduction, we will learn more about
+  these antiquotations: they greatly simplify Isabelle programming since one
+  can directly access all kinds of logical elements from ML.
+
 *}
 
 section {* Terms and Types *}
 
 text {*
-  One way to construct terms of Isabelle on the ML level is by using the antiquotation 
-  \mbox{@{text "@{term \<dots>}"}}:
+  One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
+  \mbox{@{text "@{term \<dots>}"}}. For example
 
   @{ML_response [display] "@{term \"(a::nat) + b = c\"}" 
                           "Const (\"op =\", \<dots>)  $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
@@ -292,18 +295,33 @@
   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_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
 
   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
-  (FIXME: how to construct types manually)
+  Similarly, types can be constructed for example as follows:
+
+*} 
+
+ML {*
+fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
+*}
+
+text {*
+  which can be equally written as 
+*}
+
+ML {*
+fun make_fun_type tau1 tau2 = tau1 --> tau2
+*}
+
+text {*
 
   \begin{readmore}
   There are many functions in @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
-  easier.\end{readmore}
+  and types easier.\end{readmore}
 
   Have a look at these files and try to solve the following two exercises:
 
@@ -327,14 +345,14 @@
 
 *}
 
-section {* Type Checking *}
+section {* Type-Checking *}
 
 text {* 
   
   We can freely construct and manipulate terms, since they are just
   arbitrary unchecked trees. However, we eventually want to see if a
   term is well-formed, or type checks, relative to a theory.
-  Type checking is done via the function @{ML cterm_of}, which turns 
+  Type-checking is done via the function @{ML cterm_of}, which turns 
   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   Unlike @{ML_type term}s, which are just trees, @{ML_type
   "cterm"}s are abstract objects that are guaranteed to be
@@ -386,7 +404,7 @@
    shows "Q t" (*<*)oops(*>*) 
 
 text {*
-  on the ML level:\footnote{Note that @{text "|>"} is reverse
+  on the ML-level:\footnote{Note that @{text "|>"} is reverse
   application. This combinator, and several variants are defined in
   @{ML_file "Pure/General/basics.ML"}.}
 
@@ -395,7 +413,7 @@
   val thy = @{theory}
 
   val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
-  val assm2 = cterm_of thy @{prop \"((P::nat\<Rightarrow>bool) t)\"}
+  val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}
 
   val Pt_implies_Qt = 
         assume assm1
@@ -447,14 +465,13 @@
 
   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
 
-  where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. 
+  where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open 
+  subgoals. 
   Since the goal @{term C} can potentially be an implication, there is a
   @{text "#"} wrapped around it, which prevents that premises are 
   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
   prop"} is just the identity function and used as a syntactic marker. 
   
-  (FIXME: maybe show how this is printed on the screen) 
-
   \begin{readmore}
   For more on goals see \isccite{sec:tactical-goals}. 
   \end{readmore}
@@ -476,7 +493,7 @@
   exception of possibly instantiating schematic variables. 
  
   To see how tactics work, let us transcribe a simple @{text apply}-style 
-  proof from the tutorial \cite{isa-tutorial} into ML:
+  proof from the tutorial~\cite{isa-tutorial} into ML:
 *}
 
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"




