equal
deleted
inserted
replaced
6 chapter {* Advanced Isabelle\label{chp:advanced} *} |
6 chapter {* Advanced Isabelle\label{chp:advanced} *} |
7 |
7 |
8 text {* |
8 text {* |
9 \begin{flushright} |
9 \begin{flushright} |
10 {\em All things are difficult before they are easy.} \\[1ex] |
10 {\em All things are difficult before they are easy.} \\[1ex] |
11 proverb |
11 proverb\\[2ex] |
|
12 {\em Programming is not just an act of telling a computer what |
|
13 to do: it is also an act of telling other programmers what you |
|
14 wished the computer to do. Both are important, and the latter |
|
15 deserves care.}\\[1ex] |
|
16 ---Andrew Morton, Linux Kernel mailinglist, 13 March 2012 |
12 \end{flushright} |
17 \end{flushright} |
13 |
18 |
14 \medskip |
19 \medskip |
15 While terms, types and theorems are the most basic data structures in |
20 While terms, types and theorems are the most basic data structures in |
16 Isabelle, there are a number of layers built on top of them. Most of these |
21 Isabelle, there are a number of layers built on top of them. Most of these |