equal
deleted
inserted
replaced
11 (*>*) |
11 (*>*) |
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} |
|
17 {\em ``The most effective debugging tool is still careful thought,\\ |
|
18 coupled with judiciously placed print statements.''} \\[1ex] |
|
19 Brian Kernighan, in {\em Unix for Beginners}, 1979 |
|
20 \end{flushright} |
|
21 |
|
22 \medskip |
|
23 One of the main reason for descending to the ML-level of Isabelle is to be |
16 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 |
17 able to implement automatic proof procedures. Such proof procedures can |
25 considerably lessen the burden of manual reasoning. They are centred around |
18 considerably lessen the burden of manual reasoning. They are centred around |
26 the idea of refining a goal state using tactics. This is similar to the |
19 the idea of refining a goal state using tactics. This is similar to the |
27 \isacommand{apply}-style reasoning at the user-level, where goals are |
20 \isacommand{apply}-style reasoning at the user-level, where goals are |