8 If your next project requires you to program on the ML-level of Isabelle, |
8 If your next project requires you to program on the ML-level of Isabelle, |
9 then this tutorial is for you. It will guide you through the first steps of |
9 then this tutorial is for you. It will guide you through the first steps of |
10 Isabelle programming, and also explain tricks of the trade. The best way to |
10 Isabelle programming, and also explain tricks of the trade. The best way to |
11 get to know the ML-level of Isabelle is by experimenting with the many code |
11 get to know the ML-level of Isabelle is by experimenting with the many code |
12 examples included in the tutorial. The code is as far as possible checked |
12 examples included in the tutorial. The code is as far as possible checked |
13 against the Isabelle code.\footnote{\input{version}} If something does not work, |
13 against the Isabelle distribution.\footnote{\input{version}} If something does not work, |
14 then please let us know. It is impossible for us to know every environment, |
14 then please let us know. It is impossible for us to know every environment, |
15 operating system or editor in which Isabelle is used. If you have comments, |
15 operating system or editor in which Isabelle is used. If you have comments, |
16 criticism or like to add to the tutorial, please feel free---you are most |
16 criticism or like to add to the tutorial, please feel free---you are most |
17 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
17 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
18 this we need your feedback. |
18 this we need your feedback. |
58 \begin{description} |
58 \begin{description} |
59 \item[The Isabelle sources.] They are the ultimate reference for how |
59 \item[The Isabelle sources.] They are the ultimate reference for how |
60 things really work. Therefore you should not hesitate to look at the |
60 things really work. Therefore you should not hesitate to look at the |
61 way things are actually implemented. More importantly, it is often |
61 way things are actually implemented. More importantly, it is often |
62 good to look at code that does similar things as you want to do and |
62 good to look at code that does similar things as you want to do and |
63 learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is |
63 learn from it. The UNIX command \mbox{@{text "grep -R"}} is |
64 often your best friend while programming with Isabelle, or |
64 often your best friend while programming with Isabelle, or |
65 hypersearch if you program using jEdit under MacOSX. |
65 hypersearch if you program using jEdit under MacOSX. |
66 \end{description} |
66 \end{description} |
67 |
67 |
68 *} |
68 *} |
120 *} |
120 *} |
121 |
121 |
122 section {* Some Naming Conventions in the Isabelle Sources *} |
122 section {* Some Naming Conventions in the Isabelle Sources *} |
123 |
123 |
124 text {* |
124 text {* |
125 There are a few naming conventions in Isabelle that might aid reading |
125 There are a few naming conventions in the Isabelle code that might aid reading |
126 and writing code. (Remember that code is written once, but read numerous |
126 and writing code. (Remember that code is written once, but read many |
127 times.) The most important conventions are: |
127 times.) The most important conventions are: |
128 |
128 |
129 \begin{itemize} |
129 \begin{itemize} |
130 \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term} |
130 \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term} |
131 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
131 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
168 |
168 |
169 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
169 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
170 chapter and also contributed the material on @{text NamedThmsFun}. |
170 chapter and also contributed the material on @{text NamedThmsFun}. |
171 |
171 |
172 \item {\bf Christian Sternagel} proofread the tutorial and made |
172 \item {\bf Christian Sternagel} proofread the tutorial and made |
173 comments on the text. |
173 many comments on the text. |
174 \end{itemize} |
174 \end{itemize} |
175 |
175 |
176 Please let me know of any omissions. Responsibility for any remaining |
176 Please let me know of any omissions. Responsibility for any remaining |
177 errors lies with me.\bigskip |
177 errors lies with me.\bigskip |
178 |
178 |