equal
deleted
inserted
replaced
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 students and researchers to play with Isabelle |
29 the tutorial will encourage students and researchers to play with Isabelle |
30 and implement new ideas. The source code of Isabelle can look intimidating, |
30 and implement new ideas. The source code of Isabelle can look intimidating, |
31 but beginners can get by with knowledge of only a small number functions and |
31 but beginners can get by with knowledge of only a small number of functions |
32 a few basic coding conventions. |
32 and a few basic coding conventions. |
33 |
33 |
34 |
34 |
35 The best way to get to know the ML-level of Isabelle is by experimenting |
35 The best way to get to know the ML-level of Isabelle is by experimenting |
36 with the many code examples included in the tutorial. The code is as far as |
36 with the many code examples included in the tutorial. The code is as far as |
37 possible checked against the Isabelle |
37 possible checked against the Isabelle |