equal
deleted
inserted
replaced
12 |
12 |
13 |
13 |
14 chapter {* Advanced Isabelle *} |
14 chapter {* Advanced Isabelle *} |
15 |
15 |
16 text {* |
16 text {* |
|
17 \begin{flushright} |
|
18 {\em All things are difficult before they are easy.} \\[1ex] |
|
19 proverb |
|
20 \end{flushright} |
|
21 |
|
22 \medskip |
17 While terms, types and theorems are the most basic data structures in |
23 While terms, types and theorems are the most basic data structures in |
18 Isabelle, there are a number of layers built on top of them. Most of these |
24 Isabelle, there are a number of layers built on top of them. Most of these |
19 layers are concerned with storing and manipulating data. Handling them |
25 layers are concerned with storing and manipulating data. Handling them |
20 properly is an essential skill for programming on the ML-level of Isabelle |
26 properly is an essential skill for programming on the ML-level of Isabelle |
21 programming. The most basic layer are theories. They contain global data and |
27 programming. The most basic layer are theories. They contain global data and |