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 recent versions of Isabelle. If something does not work, then please |
13 against \input{version}. If something does not work, |
14 let us know. It is impossible for us to know every environment, operating |
14 then please let us know. It is impossible for us to know every environment, |
15 system or editor in which Isabelle is used. If you have comments, criticism |
15 operating system or editor in which Isabelle is used. If you have comments, |
16 or like to add to the tutorial, please feel free---you are most welcome! The |
16 criticism or like to add to the tutorial, please feel free---you are most |
17 tutorial is meant to be gentle and comprehensive. To achieve this we need |
17 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
18 your feedback. |
18 this we need your feedback. |
19 *} |
19 *} |
20 |
20 |
21 section {* Intended Audience and Prior Knowledge *} |
21 section {* Intended Audience and Prior Knowledge *} |
22 |
22 |
23 text {* |
23 text {* |
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 @{text "grep -R"} is |
63 learn from it. The GNU/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 use jEdit under MacOSX. |
65 hypersearch if you program using jEdit under MacOSX. |
66 \end{description} |
66 \end{description} |
67 |
67 |
68 *} |
68 *} |
69 |
69 |
70 section {* Typographic Conventions in the Tutorial *} |
70 section {* Typographic Conventions in the Tutorial *} |
134 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
134 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
135 \item @{text thy} for theories; ML-type: @{ML_type theory} |
135 \item @{text thy} for theories; ML-type: @{ML_type theory} |
136 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
136 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
137 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
137 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
138 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
138 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
|
139 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
139 \end{itemize} |
140 \end{itemize} |
140 *} |
141 *} |
141 |
142 |
142 section {* Acknowledgements *} |
143 section {* Acknowledgements *} |
143 |
144 |