ProgTutorial/Intro.thy
changeset 353 e73ccbed776e
parent 346 0fea8b7a14a1
child 356 43df2d59fb98
equal deleted inserted replaced
352:9f12e53eb121 353:e73ccbed776e
    23   \end{flushright}
    23   \end{flushright}
    24 
    24 
    25   \medskip
    25   \medskip
    26   If your next project requires you to program on the ML-level of Isabelle,
    26   If your next project requires you to program on the ML-level of Isabelle,
    27   then this tutorial is for you. It will guide you through the first steps of
    27   then this tutorial is for you. It will guide you through the first steps of
    28   Isabelle programming, and also explain tricks of the trade. The best way to
    28   Isabelle programming, and also explain tricks of the trade. We also hope
       
    29   the tutorial will encourage researchers to play with Isabelle. The best way to
    29   get to know the ML-level of Isabelle is by experimenting with the many code
    30   get to know the ML-level of Isabelle is by experimenting with the many code
    30   examples included in the tutorial. The code is as far as possible checked
    31   examples included in the tutorial. The code is as far as possible checked
    31   against the Isabelle distribution.\footnote{\input{version}} If something does not work, 
    32   against the Isabelle distribution.\footnote{\input{version}} If something does not work, 
    32   then please let us know. It is impossible for us to know every environment, 
    33   then please let us know. It is impossible for us to know every environment, 
    33   operating system or editor in which Isabelle is used. If you have comments, 
    34   operating system or editor in which Isabelle is used. If you have comments,