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 {* Isabelle -- The Good, the Bad and the Ugly *} |
5 chapter {* Let's Talk About the Good, the Bad and the Ugly *} |
6 |
6 |
7 text {* |
7 text {* |
8 Isabelle is build around a few central ideas. One is the LCF-approach to |
8 Isabelle is build around a few central ideas. One is the LCF-approach to |
9 theorem proving where there is a small trusted core and everything else is |
9 theorem proving where there is a small trusted core and everything else is |
10 build on top of this trusted core. The central data structures involved |
10 build on top of this trusted core. The central data structures involved |