ProgTutorial/Intro.thy
changeset 324 4172c0743cf2
parent 306 fe732e890d87
child 328 c0cae24b9d46
equal deleted inserted replaced
323:92f6a772e013 324:4172c0743cf2
    10   {\em
    10   {\em
    11   ``My thesis is that programming is not at the bottom of the intellectual \\
    11   ``My thesis is that programming is not at the bottom of the intellectual \\
    12   pyramid, but at the top. It's creative design of the highest order. It \\
    12   pyramid, but at the top. It's creative design of the highest order. It \\
    13   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
    13   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
    14   claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
    14   claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
    15   Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
    15   Richard Bornat, In {\em Defence of Programming}. \cite{Bornat-lecture}
    16   \end{flushright}
    16   \end{flushright}
    17 
    17 
    18   \medskip
    18   \medskip
    19   If your next project requires you to program on the ML-level of Isabelle,
    19   If your next project requires you to program on the ML-level of Isabelle,
    20   then this tutorial is for you. It will guide you through the first steps of
    20   then this tutorial is for you. It will guide you through the first steps of