equal
deleted
inserted
replaced
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 *} |
69 |
69 |
70 section {* Typographic Conventions in the Tutorial *} |
70 section {* Typographic Conventions *} |
71 |
71 |
72 text {* |
72 text {* |
73 |
73 |
74 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 |
75 ML-expression: |
75 ML-expression: |
117 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 |
118 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 |
119 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 *} |
120 *} |
121 |
121 |
122 section {* 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 Isabelle 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 numerous |
127 times.) The most important conventions are: |
127 times.) The most important conventions are: |