equal
deleted
inserted
replaced
12 |
12 |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
14 |
14 |
15 text {* |
15 text {* |
16 \begin{flushright} |
16 \begin{flushright} |
17 {\em ``The most effective debugging tool is still careful thought, coupled with |
17 {\em ``The most effective debugging tool is still careful thought,\\ |
18 judiciously placed print statements.''} \\[1ex] |
18 coupled with judiciously placed print statements.''} \\[1ex] |
19 Brian Kernighan |
19 Brian Kernighan, in {\em Unix for Beginners}, 1979 |
20 \end{flushright} |
20 \end{flushright} |
21 |
21 |
22 \medskip |
22 \medskip |
23 One of the main reason for descending to the ML-level of Isabelle is to be |
23 One of the main reason for descending to the ML-level of Isabelle is to be |
24 able to implement automatic proof procedures. Such proof procedures can |
24 able to implement automatic proof procedures. Such proof procedures can |