equal
deleted
inserted
replaced
12 Isabelle programming, and also explain tricks of the trade. The best way to |
12 Isabelle programming, and also explain tricks of the trade. The best way to |
13 get to know the ML-level of Isabelle is by experimenting with the many code |
13 get to know the ML-level of Isabelle is by experimenting with the many code |
14 examples included in the tutorial. The code is as far as possible checked |
14 examples included in the tutorial. The code is as far as possible checked |
15 against recent versions of Isabelle. If something does not work, then |
15 against recent versions of Isabelle. If something does not work, then |
16 please let us know. If you have comments, criticism or like to add to the |
16 please let us know. If you have comments, criticism or like to add to the |
17 tutorial, feel free---you are most welcome! The tutorial is meant to be |
17 tutorial, please feel free---you are most welcome! The tutorial is meant to be |
18 gentle and comprehensive. To achieve this we need your feedback. |
18 gentle and comprehensive. To achieve 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 |
36 |
36 |
37 The following documentation about Isabelle programming already exists (and is |
37 The following documentation about Isabelle programming already exists (and is |
38 part of the distribution of Isabelle): |
38 part of the distribution of Isabelle): |
39 |
39 |
40 \begin{description} |
40 \begin{description} |
41 \item[The Implementation Manual] describes Isabelle |
41 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
42 from a high-level perspective, documenting both the underlying |
42 from a high-level perspective, documenting both the underlying |
43 concepts and some of the interfaces. |
43 concepts and some of the interfaces. |
44 |
44 |
45 \item[The Isabelle Reference Manual] is an older document that used |
45 \item[The Isabelle Reference Manual] is an older document that used |
46 to be the main reference of Isabelle at a time when all proof scripts |
46 to be the main reference of Isabelle at a time when all proof scripts |
108 Further information or pointers to files. |
108 Further information or pointers to files. |
109 \end{readmore} |
109 \end{readmore} |
110 |
110 |
111 A few exercises a scattered around the text. Their solutions are given |
111 A few exercises a scattered around the text. Their solutions are given |
112 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
112 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
113 to solve the exercises on your own. |
113 to solve the exercises on your own, and then look at the solutions. |
114 |
114 |
115 *} |
115 *} |
116 |
116 |
117 section {* Acknowledgements *} |
117 section {* Acknowledgements *} |
118 |
118 |