--- a/CookBook/FirstSteps.thy	Mon Oct 06 10:11:08 2008 -0400
+++ b/CookBook/FirstSteps.thy	Thu Oct 09 12:58:50 2008 -0400
@@ -168,10 +168,11 @@
   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 theorems:
+  In a similar way you can use antiquotations to refer to theorems or simpsets:
 *}
 
 ML {* @{thm allI} *}
+ML {* @{simpset} *}
 
 text {*
   In the course of this introduction, we will learn more about 
@@ -412,7 +413,7 @@
    shows "Q t" (*<*)oops(*>*) 
 
 text {*
-  on the ML level:\footnote{Note that @{text "|>"} is just 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"}.}
 
@@ -440,6 +441,22 @@
 
 text {*
 
+  This code-snippet constructs the following proof:
+
+  \[
+  \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
+    {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+       {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
+          {\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+                 {\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
+                 &
+           \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
+          }
+       }
+    }
+  \]
+
+
   \begin{readmore}
   For how the functions @{text "assume"}, @{text "forall_elim"} etc work
   see \isccite{sec:thms}. The basic functions for theorems are defined in
@@ -468,6 +485,8 @@
   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}
@@ -502,13 +521,12 @@
 
 
 text {*
-  
-  To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
-  sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
-  the variables @{text params} that will be generalised once the
-  goal is proved; @{text "tac"} is a function that returns a tactic having some funny 
-  input parameters (FIXME by possibly having an explanation in the implementation-manual). 
-
+  To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets 
+  up a goal state for proving the goal @{text C} under the assumptions @{text As} 
+  (empty in the proof at hand) 
+  with the variables @{text xs} that will be generalised once the
+  goal is proved. The @{text "tac"} is the tactic which proves the goal and which 
+  can make use of the local assumptions.
 *}
 
 
@@ -527,6 +545,15 @@
 end
 *}
 
+text {*
+
+  \begin{readmore}
+  To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
+  \end{readmore}
+
+*}
+
+
 text {* An alternative way to transcribe this proof is as follows *}
 
 ML {*
@@ -543,10 +570,11 @@
 end
 *}
 
+text {* (FIXME: are there any advantages/disadvantages about this way?) *}
+
 section {* Storing Theorems *}
 
 section {* Theorem Attributes *}
 
-text {* Was changing theorems. *}
 
 end
\ No newline at end of file