equal
deleted
inserted
replaced
11 (*>*) |
11 (*>*) |
12 |
12 |
13 chapter {* First Steps\label{chp:firststeps} *} |
13 chapter {* First Steps\label{chp:firststeps} *} |
14 |
14 |
15 text {* |
15 text {* |
16 \begin{flushright} |
16 \begin{flushright} |
17 {\em |
17 {\em ``The most effective debugging tool is still careful thought,\\ |
18 ``We will most likely never realize the full importance of painting the Tower,\\ |
18 coupled with judiciously placed print statements.''} \\[1ex] |
19 that it is the essential element in the conservation of metal works and the\\ |
19 Brian Kernighan, in {\em Unix for Beginners}, 1979 |
20 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] |
|
21 Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been |
|
22 re-painted 18 times since its initial construction, an average of once every |
|
23 seven years. It takes more than one year for a team of 25 painters to paint the tower |
|
24 from top to bottom.} |
|
25 \end{flushright} |
20 \end{flushright} |
26 |
21 |
27 \medskip |
22 \medskip |
28 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for |
23 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for |
29 Isabelle must be part of a theory. If you want to follow the code given in |
24 Isabelle must be part of a theory. If you want to follow the code given in |