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 |
|
18 ``The first thing I would say is that when you write a program, think of\\ |
|
19 it primarily as a work of literature. You're trying to write something\\ |
|
20 that human beings are going to read. Don't think of it primarily as\\ |
|
21 something a computer is going to follow. The more effective you are\\ |
|
22 at making your program readable, the more effective it's going to\\ |
|
23 be: You'll understand it today, you'll understand it next week, and\\ |
|
24 your successors who are going to maintain and modify it will\\ |
|
25 understand it.''}\\[1ex] |
|
26 Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996. |
|
27 \end{flushright} |
|
28 |
16 One of the main reason for descending to the ML-level of Isabelle is to be |
29 One of the main reason for descending to the ML-level of Isabelle is to be |
17 able to implement automatic proof procedures. Such proof procedures can |
30 able to implement automatic proof procedures. Such proof procedures can |
18 considerably lessen the burden of manual reasoning. They are centred around |
31 considerably lessen the burden of manual reasoning. They are centred around |
19 the idea of refining a goal state using tactics. This is similar to the |
32 the idea of refining a goal state using tactics. This is similar to the |
20 \isacommand{apply}-style reasoning at the user-level, where goals are |
33 \isacommand{apply}-style reasoning at the user-level, where goals are |