equal
deleted
inserted
replaced
1 theory General |
1 theory General |
2 imports Base FirstSteps |
2 imports Base FirstSteps |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Let's Talk About the Good, the Bad and the Ugly *} |
5 (*<*) |
|
6 setup{* |
|
7 open_file_with_prelude |
|
8 "General_Code.thy" |
|
9 ["theory General", "imports Base FirstSteps", "begin"] |
|
10 *} |
|
11 (*>*) |
|
12 |
|
13 |
|
14 chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *} |
6 |
15 |
7 text {* |
16 text {* |
8 Isabelle is build around a few central ideas. One central idea is the |
17 Isabelle is build around a few central ideas. One central idea is the |
9 LCF-approach to theorem proving where there is a small trusted core and |
18 LCF-approach to theorem proving where there is a small trusted core and |
10 everything else is build on top of this trusted core. The fundamental data |
19 everything else is build on top of this trusted core. The fundamental data |