equal
deleted
inserted
replaced
10 {\em An important principle underlying the success and popularity of Unix\\ is |
10 {\em An important principle underlying the success and popularity of Unix\\ is |
11 the philosophy of building on the work of others.} \\[1ex] |
11 the philosophy of building on the work of others.} \\[1ex] |
12 Tony Travis in an email about the\\ ``LINUX is obsolete'' debate |
12 Tony Travis in an email about the\\ ``LINUX is obsolete'' debate |
13 \end{flushright} |
13 \end{flushright} |
14 |
14 |
|
15 \begin{flushright} |
|
16 {\em |
|
17 Document your code as if someone else might have to take it over at any |
|
18 moment and know what to do with it. That person might actually be you -- |
|
19 how often have you had to revisit your own code and thought to yourself, |
|
20 what was I trying to do here?} \\[1ex] |
|
21 Phil Chu in ``Seven Habits of Highly Effective Programmers'' |
|
22 \end{flushright} |
15 |
23 |
16 Isabelle distinguishes between \emph{outer} and \emph{inner} |
24 Isabelle distinguishes between \emph{outer} and \emph{inner} |
17 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
25 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
18 and so on, belong to the outer syntax, whereas terms, types and so on belong |
26 and so on, belong to the outer syntax, whereas terms, types and so on belong |
19 to the inner syntax. For parsing inner syntax, Isabelle uses a rather |
27 to the inner syntax. For parsing inner syntax, Isabelle uses a rather |