ProgTutorial/Intro.thy
changeset 530 aabb4c93a6ed
parent 529 13d7ea419c5f
child 532 8411f242e094
equal deleted inserted replaced
529:13d7ea419c5f 530:aabb4c93a6ed
   286   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 
   286   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 
   287   and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   287   and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   288   are by him.
   288   are by him.
   289 
   289 
   290   \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
   290   \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
   291   parsers and contributed exercise \ref{ex:contextfree} and contributed 
   291   parsers, contributed exercise \ref{ex:contextfree} and contributed 
   292   ``introspection'' of theorems 
   292   to the ``introspection'' of theorems in section \ref{sec:theorems}.
   293   \ref{sec:theorems}.
       
   294 
   293 
   295 
   294 
   296   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
   295   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
   297   about parsing.
   296   about parsing.
   298 
   297 
   299   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
   298   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
   300 
   299 
   301   \item {\bf Rafal Kolanski} contributed the ``introspection'' of theorems 
   300   \item {\bf Rafal Kolanski} contributed to the ``introspection'' of theorems 
   302   \ref{sec:theorems}.
   301   in section \ref{sec:theorems}.
   303 
   302 
   304   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
   303   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
   305   chapter and also contributed the material on @{ML_funct Named_Thms}.
   304   chapter and also contributed the material on @{ML_funct Named_Thms}.
   306 
   305 
   307   \item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.
   306   \item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.