--- a/ProgTutorial/Essential.thy	Thu Jun 21 08:39:02 2012 +0100
+++ b/ProgTutorial/Essential.thy	Thu Jun 21 11:08:02 2012 +0100
@@ -1966,11 +1966,12 @@
 
  
 text {*
-  One often wants to know the theorems that are involved in proving 
-  a theorem. They can be obtained by introspecting the theorem.
-  To introspect a theorem, let us define the following three functions that 
-  analyse the @{ML_type_ind proof_body} data-structure from the structure 
-  @{ML_struct Proofterm}.
+  Sometimes one wants to know the theorems that are involved in
+  proving a theorem, especially when the proof is by @{text
+  auto}. These theorems can be obtained by introspecting the proved theorem.
+  To introspect a theorem, let us define the following three functions
+  that analyse the @{ML_type_ind proof_body} data-structure from the
+  structure @{ML_struct Proofterm}.
 *}
 
 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
@@ -2032,8 +2033,8 @@
   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
   \"Pure.protectI\"]"}
 
-  The theorems @{thm [source] protectD} and @{thm [source]
-  protectI} that are internal theorems are always part of a
+  The theorems @{thm [source] Pure.protectD} and @{thm [source]
+  Pure.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.
 
@@ -2077,6 +2078,11 @@
   "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
   \"Pure.protectI\"]"}
 
+  \begin{exercise}
+  Have a look at the theorems that are used when a lemma is ``proved''
+  by \isacommand{sorry}? 
+  \end{exercise}
+
   \begin{readmore} 
   The data-structure @{ML_type proof_body} is implemented
   in the file @{ML_file "Pure/proofterm.ML"}. The implementation 

Binary file progtutorial.pdf has changed