equal
deleted
inserted
replaced
1 theory Intro |
1 theory Intro |
2 imports Base |
2 imports Base |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Introduction *} |
5 chapter {* Introduction *} |
|
6 |
6 |
7 |
7 text {* |
8 text {* |
8 \begin{flushright} |
9 \begin{flushright} |
9 {\em |
10 {\em |
10 ``My thesis is that programming is not at the bottom of the intellectual \\ |
11 ``My thesis is that programming is not at the bottom of the intellectual \\ |
20 Isabelle programming, and also explain ``tricks of the trade''. We also hope |
21 Isabelle programming, and also explain ``tricks of the trade''. We also hope |
21 the tutorial will encourage students and researchers to play with Isabelle |
22 the tutorial will encourage students and researchers to play with Isabelle |
22 and implement new ideas. The source code of Isabelle can look intimidating, |
23 and implement new ideas. The source code of Isabelle can look intimidating, |
23 but beginners can get by with knowledge of only a handful of concepts, |
24 but beginners can get by with knowledge of only a handful of concepts, |
24 a small number of functions and a few basic coding conventions. |
25 a small number of functions and a few basic coding conventions. |
25 |
26 There is also a considerable amount of code written in Scala that allows |
|
27 Isabelle interface with the Jedit GUI. Explanation of this part is beyond |
|
28 this tutorial. |
26 |
29 |
27 The best way to get to know the ML-level of Isabelle is by experimenting |
30 The best way to get to know the ML-level of Isabelle is by experimenting |
28 with the many code examples included in the tutorial. The code is as far as |
31 with the many code examples included in the tutorial. The code is as far as |
29 possible checked against the Isabelle |
32 possible checked against the Isabelle |
30 distribution.%%\footnote{\input{version.tex}} |
33 distribution.%%\footnote{\input{version.tex}} |