# HG changeset patch # User Christian Urban # Date 1340178818 -3600 # Node ID aabb4c93a6edc1591fa1940e57826b3526b158f5 # Parent 13d7ea419c5f6889b156d29165d1933021940935 tuned diff -r 13d7ea419c5f -r aabb4c93a6ed ProgTutorial/Essential.thy --- 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}. diff -r 13d7ea419c5f -r aabb4c93a6ed ProgTutorial/Intro.thy --- 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}. diff -r 13d7ea419c5f -r aabb4c93a6ed progtutorial.pdf Binary file progtutorial.pdf has changed