--- a/CookBook/FirstSteps.thy	Sun Oct 05 14:29:13 2008 -0400
+++ b/CookBook/FirstSteps.thy	Mon Oct 06 10:11:08 2008 -0400
@@ -24,7 +24,7 @@
   \end{center}
 *}
 
-section {* Inluding ML-Code *}
+section {* Including ML-Code *}
 
 text {*
   The easiest and quickest way to include code in a theory is
@@ -292,7 +292,7 @@
 text {*
 
   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.
+  @{term "tau"} into an antiquotation. For example the following does not work.
 *}
 
 ML {*
@@ -323,6 +323,8 @@
 
   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
+  (FIXME: how to construct types manually)
+
   \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 
@@ -362,7 +364,7 @@
   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
-  type-correct, and can only be constructed via the official
+  type-correct, and that can only be constructed via the official
   interfaces.
 
   Type checking is always relative to a theory context. For now we can use
@@ -372,6 +374,8 @@
 
 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}
 
+text {* and *}
+
 ML {*
   let
     val natT = @{typ "nat"}
@@ -459,7 +463,6 @@
   @{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. 
-
   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>
@@ -540,6 +543,10 @@
 end
 *}
 
-section {* Storing and Changing Theorems and so on *}
+section {* Storing Theorems *}
+
+section {* Theorem Attributes *}
+
+text {* Was changing theorems. *}
 
 end
\ No newline at end of file