ProgTutorial/Intro.thy
changeset 520 615762b8d8cb
parent 517 d8c376662bb4
child 521 9728b0432fb2
equal deleted inserted replaced
519:cf471fa86091 520:615762b8d8cb
   291   parsers and contributed exercise \ref{ex:contextfree}.
   291   parsers and contributed exercise \ref{ex:contextfree}.
   292 
   292 
   293   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
   293   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
   294   about parsing.
   294   about parsing.
   295 
   295 
       
   296   \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
       
   297   @{text "command_spec"}, which simplified the code. 
       
   298 
   296   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
   299   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
   297 
   300 
   298   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
   301   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
   299   chapter and also contributed the material on @{ML_funct Named_Thms}.
   302   chapter and also contributed the material on @{ML_funct Named_Thms}.
   300 
   303