14 chapter {* Advanced Isabelle *} |
14 chapter {* Advanced Isabelle *} |
15 |
15 |
16 text {* |
16 text {* |
17 While terms, types and theorems are the most basic data structures in |
17 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 |
18 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 |
19 layers are concerned with storing and manipulating data. Handling them |
20 them properly is an essential skill for Isabelle programming. The most basic |
20 properly is an essential skill for programming on the ML-level of Isabelle |
21 layer are theories. They contain global data and can be seen as the |
21 programming. The most basic layer are theories. They contain global data and |
22 ``long-term memory'' of Isabelle. There is usually only one theory |
22 can be seen as the ``long-term memory'' of Isabelle. There is usually only |
23 active at each moment. Proof contexts and local theories, on the |
23 one theory active at each moment. Proof contexts and local theories, on the |
24 other hand, store local data for a task at hand. They act like the |
24 other hand, store local data for a task at hand. They act like the |
25 ``short-term memory'' and there can be many of them that are active |
25 ``short-term memory'' and there can be many of them that are active in |
26 in parallel. |
26 parallel. |
27 *} |
27 *} |
28 |
28 |
29 section {* Theories\label{sec:theories} (TBD) *} |
29 section {* Theories\label{sec:theories} (TBD) *} |
30 |
30 |
31 text {* |
31 text {* |