equal
deleted
inserted
replaced
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 and implement |
29 the tutorial will encourage researchers to play with Isabelle and implement |
30 new ideas. The sources of Isabelle can look intimidating, but beginners |
30 new ideas. The source code of Isabelle can look intimidating, but beginners |
31 can get by with knowledge of only a small number functions and a few basic |
31 can get by with knowledge of only a small number functions and a few basic |
32 coding conventions. |
32 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 |