24 |
24 |
25 \medskip |
25 \medskip |
26 If your next project requires you to program on the ML-level of Isabelle, |
26 If your next project requires you to program on the ML-level of Isabelle, |
27 then this tutorial is for you. It will guide you through the first steps of |
27 then this tutorial is for you. It will guide you through the first steps of |
28 Isabelle programming, and also explain tricks of the trade. We also hope |
28 Isabelle programming, and also explain tricks of the trade. We also hope |
29 the tutorial will encourage researchers to play with Isabelle. The best way to |
29 the tutorial will encourage researchers to play with Isabelle and implement |
30 get to know the ML-level of Isabelle is by experimenting with the many code |
30 new ideas. The sources of Isabelle can look intimidating, but beginners |
31 examples included in the tutorial. The code is as far as possible checked |
31 can get by with knowledge of only a small number functions and a few basic |
32 against the Isabelle distribution.\footnote{\input{version}} If something does not work, |
32 coding conventions. |
33 then please let us know. It is impossible for us to know every environment, |
33 |
34 operating system or editor in which Isabelle is used. If you have comments, |
34 |
35 criticism or like to add to the tutorial, please feel free---you are most |
35 The best way to get to know the ML-level of Isabelle is by experimenting |
36 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
36 with the many code examples included in the tutorial. The code is as far as |
|
37 possible checked against the Isabelle |
|
38 distribution.\footnote{\input{version}} If something does not work, then |
|
39 please let us know. It is impossible for us to know every environment, |
|
40 operating system or editor in which Isabelle is used. If you have comments, |
|
41 criticism or like to add to the tutorial, please feel free---you are most |
|
42 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
37 this we need your feedback. |
43 this we need your feedback. |
38 *} |
44 *} |
39 |
45 |
40 section {* Intended Audience and Prior Knowledge *} |
46 section {* Intended Audience and Prior Knowledge *} |
41 |
47 |