58 \begin{description} |
58 \begin{description} |
59 \item[The code.] It is the ultimate reference for how |
59 \item[The code.] It is 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 UNIX command @{text "grep -R"} is |
63 learn from it. The GNU/UNIX command @{text "grep -R"} is |
64 often your best friend while programming with Isabelle. |
64 often your best friend while programming with Isabelle, or |
|
65 hypersearch if you use jEdit under MacOSX. |
65 \end{description} |
66 \end{description} |
66 |
67 |
67 *} |
68 *} |
68 |
69 |
69 section {* Typographic Conventions *} |
70 section {* Typographic Conventions in the Tutorial *} |
70 |
71 |
71 text {* |
72 text {* |
72 |
73 |
73 All ML-code in this tutorial is typeset in shaded boxes, like the following |
74 All ML-code in this tutorial is typeset in shaded boxes, like the following |
74 ML-expression: |
75 ML-expression: |
114 {http://isabelle.in.tum.de/repos/isabelle/}. |
115 {http://isabelle.in.tum.de/repos/isabelle/}. |
115 |
116 |
116 A few exercises are scattered around the text. Their solutions are given |
117 A few exercises are scattered around the text. Their solutions are given |
117 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
118 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
118 to solve the exercises on your own, and then look at the solutions. |
119 to solve the exercises on your own, and then look at the solutions. |
|
120 *} |
119 |
121 |
|
122 section {* Naming Conventions in the Isabelle Sources *} |
|
123 |
|
124 text {* |
|
125 There are a few naming conventions in Isabelle that might aid reading |
|
126 and writing code. (Remember that code is written once, but read numerous |
|
127 times.) The most important conventions are: |
|
128 |
|
129 \begin{itemize} |
|
130 \item @{text t}, @{text u} for (raw) terms, @{ML_type term} |
|
131 \item @{text ct}, @{text cu} for certified terms, @{ML_type cterm} |
|
132 \item @{text "ty"}, @{text T}, @{text U} for (raw) types, @{ML_type typ} |
|
133 \item @{text th}, @{text thm} for theorems, @{ML_type thm} |
|
134 \item @{text "foo_tac"} for tactics, @{ML_type tactic} |
|
135 \item @{text thy} for theories, @{ML_type theory} |
|
136 \item @{text ctxt} for proof contexts, @{ML_type Proof.context} |
|
137 \item @{text lthy} for local theories, @{ML_type local_theory} |
|
138 \item @{text context} for generic contextx, @{ML_type Context.generic} |
|
139 \end{itemize} |
120 *} |
140 *} |
121 |
141 |
122 section {* Acknowledgements *} |
142 section {* Acknowledgements *} |
123 |
143 |
124 text {* |
144 text {* |
150 \end{itemize} |
170 \end{itemize} |
151 |
171 |
152 Please let me know of any omissions. Responsibility for any remaining |
172 Please let me know of any omissions. Responsibility for any remaining |
153 errors lies with me.\bigskip |
173 errors lies with me.\bigskip |
154 |
174 |
|
175 \vspace{5cm} |
155 {\Large\bf |
176 {\Large\bf |
156 This document is still in the process of being written! All of the |
177 This document is still in the process of being written! All of the |
157 text is still under construction. Sections and |
178 text is still under construction. Sections and |
158 chapters that are under \underline{heavy} construction are marked |
179 chapters that are under \underline{heavy} construction are marked |
159 with TBD.} |
180 with TBD.} |