equal
deleted
inserted
replaced
7 |
7 |
8 text {* |
8 text {* |
9 \begin{flushright} |
9 \begin{flushright} |
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 Linus Torwalds in the email exchange\\ with Andrew S.~Tannenbaum |
12 Tony Travis in an email about the\\ ``LINUX is obsolete'' debate |
13 \end{flushright} |
13 \end{flushright} |
14 |
14 |
15 |
15 |
16 Isabelle distinguishes between \emph{outer} and \emph{inner} |
16 Isabelle distinguishes between \emph{outer} and \emph{inner} |
17 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
17 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |