--- a/ProgTutorial/Recipes/Introspection.thy	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Recipes/Introspection.thy	Wed Jun 20 08:29:12 2012 +0100
@@ -61,7 +61,7 @@
   whereby @{text "Introspection"} refers to the theory name in which
   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
   proof_body_of in Thm} returns a part of the data that is stored in a
-  theorem.  Notice that the apply-proof of this theorem references
+  theorem.  Notice that the first proof above references
   three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 
   and @{thm [source] conjunct2}. We can obtain them by descending into the
   first level of the proof-tree, as follows.
@@ -75,8 +75,8 @@
   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
   \"Pure.protectI\"]"}
 
-  Note the theorems @{thm [source] protectD} and @{thm [source]
-  protectI} that are internal theorems which are always part of a
+  The theorems @{thm [source] protectD} and @{thm [source]
+  protectI} that are internal theorems are always part of a
   proof in Isabelle. Note also that applications of @{text assumption} do not
   count as a separate theorem, as you can see in the following code.
 
@@ -90,7 +90,8 @@
 
   Interestingly, but not surprisingly, the proof of @{thm [source]
   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
-  and @{thm [source] my_conjIb}, as can be seen next.
+  and @{thm [source] my_conjIb}, as can be seen by the theorems that
+  are returned for @{thm [source] my_conjIc}.
 
   @{ML_response [display,gray]
   "@{thm my_conjIc}
@@ -103,7 +104,7 @@
   \"Pure.protectI\"]"}
 
   Of course we can also descend into the second level of the tree 
-  ``behind'' @{thm [source] my_conjIa}, which
+  ``behind'' @{thm [source] my_conjIa} say, which
   means we obtain the theorems that are used in order to prove
   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.