--- a/ProgTutorial/Essential.thy	Wed Jun 20 08:29:12 2012 +0100
+++ b/ProgTutorial/Essential.thy	Wed Jun 20 08:53:38 2012 +0100
@@ -1966,8 +1966,8 @@
 
  
 text {*
-  One often wants to know the theorems that are used in the proof 
-  of a theorem. They can be obtained by introspecting the theorem.
+  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}.

--- a/ProgTutorial/Intro.thy	Wed Jun 20 08:29:12 2012 +0100
+++ b/ProgTutorial/Intro.thy	Wed Jun 20 08:53:38 2012 +0100
@@ -288,9 +288,8 @@
   are by him.
 
   \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
-  parsers and contributed exercise \ref{ex:contextfree} and contributed 
-  ``introspection'' of theorems 
-  \ref{sec:theorems}.
+  parsers, contributed exercise \ref{ex:contextfree} and contributed 
+  to the ``introspection'' of theorems in section \ref{sec:theorems}.
 
 
   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
@@ -298,8 +297,8 @@
 
   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
 
-  \item {\bf Rafal Kolanski} contributed the ``introspection'' of theorems 
-  \ref{sec:theorems}.
+  \item {\bf Rafal Kolanski} contributed to the ``introspection'' of theorems 
+  in section \ref{sec:theorems}.
 
   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
   chapter and also contributed the material on @{ML_funct Named_Thms}.

Binary file progtutorial.pdf has changed