--- a/CookBook/FirstSteps.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -226,17 +226,17 @@
 
   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
-  Consider for example
+  Consider for example the pairs
 
   @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
  
-  which inserts the coercion in the second component and 
+  where an coercion is inserted in the second component and 
 
   @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 
-  which does not (since it is already constructed using the meta-implication). 
+  where it is not (since it is already constructed using the meta-implication). 
 
   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
 
@@ -281,36 +281,39 @@
 
 text {*
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
-  to both functions: 
+  to both functions. With @{ML make_imp} we obtain the correct term involving 
+  @{term "S"}, @{text "T"} and  @{text "@{typ nat}"} 
 
   @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" 
     "Const \<dots> $ 
     Abs (\"x\", Type (\"nat\",[]),
       Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
                   (Free (\"T\",\<dots>) $ \<dots>))"}
+
+  With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} 
+  and @{text "Q"} from the antiquotation.
+
   @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
     "Const \<dots> $ 
     Abs (\"x\", \<dots>,
       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  As can be seen, in the first case the arguments are correctly used, while the 
-  second generates a term involving the @{term "P"} and @{text "Q"} from the 
-  antiquotation.
+  One tricky point in constructing terms by hand is to obtain the fully
+  qualified name for constants. For example the names for @{text "zero"} and
+  @{text "+"} are more complex than one first expects, namely
 
-  One tricky point in constructing terms by hand is to obtain the 
-  fully qualified name for constants. For example the names for @{text "zero"} and
-  @{text "+"} are more complex than one first expects, namely 
 
   \begin{center}
   @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. 
   \end{center}
   
-  The extra prefixes @{text zero_class} and @{text plus_class} are present because 
-  these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
-  which theory they are defined. Guessing such internal names can sometimes be quite hard. 
-  Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
-  expansion automatically, for example:
+  The extra prefixes @{text zero_class} and @{text plus_class} are present
+  because these constants are defined within type classes; the prefix @{text
+  "HOL"} indicates in which theory they are defined. Guessing such internal
+  names can sometimes be quite hard. Therefore Isabelle provides the
+  antiquotation @{text "@{const_name \<dots>}"} which does the expansion
+  automatically, for example:
 
   @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
 
@@ -575,6 +578,11 @@
 section {* Theorem Attributes *}
 
 
+section {* Combinators *}
 
+text {*
+  @{text I}, @{text K}
+  
+*}
 
 end
\ No newline at end of file