equal
deleted
inserted
replaced
12 |
12 |
13 |
13 |
14 chapter {* Isabelle Essentials *} |
14 chapter {* Isabelle Essentials *} |
15 |
15 |
16 text {* |
16 text {* |
|
17 \begin{flushright} |
|
18 {\em One man's obfuscation is another man's abstraction.} \\[1ex] |
|
19 Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ |
|
20 24~Nov.~2009 |
|
21 \end{flushright} |
|
22 |
|
23 \medskip |
17 Isabelle is build around a few central ideas. One central idea is the |
24 Isabelle is build around a few central ideas. One central idea is the |
18 LCF-approach to theorem proving where there is a small trusted core and |
25 LCF-approach to theorem proving where there is a small trusted core and |
19 everything else is build on top of this trusted core |
26 everything else is built on top of this trusted core |
20 \cite{GordonMilnerWadsworth79}. The fundamental data |
27 \cite{GordonMilnerWadsworth79}. The fundamental data |
21 structures involved in this core are certified terms and certified types, |
28 structures involved in this core are certified terms and certified types, |
22 as well as theorems. |
29 as well as theorems. |
23 *} |
30 *} |
24 |
31 |