55 were written on the ML-level. Many parts of this manual are outdated |
55 were written on the ML-level. Many parts of this manual are outdated |
56 now, but some parts, particularly the chapters on tactics, are still |
56 now, but some parts, particularly the chapters on tactics, are still |
57 useful. |
57 useful. |
58 |
58 |
59 \item[The Isar Reference Manual] provides specification material (like grammars, |
59 \item[The Isar Reference Manual] provides specification material (like grammars, |
60 examples and so on) about Isar and its implementation. It is currently in |
60 examples and so on) about Isar and its implementation. |
61 the process of being updated. |
|
62 \end{description} |
61 \end{description} |
63 |
62 |
64 Then of course there are: |
63 Then of course there are: |
65 |
64 |
66 \begin{description} |
65 \begin{description} |
150 or dead-ends in the Isabelle development. Of course this means also you have |
149 or dead-ends in the Isabelle development. Of course this means also you have |
151 to synchronise your code at the next stable release. Another possibility |
150 to synchronise your code at the next stable release. Another possibility |
152 is to get your code into the Isabelle distribution. For this you have |
151 is to get your code into the Isabelle distribution. For this you have |
153 to convince other developers that your code or project is of general interest. |
152 to convince other developers that your code or project is of general interest. |
154 If you managed to do this, then the problem of the moving target goes |
153 If you managed to do this, then the problem of the moving target goes |
155 away, because when checking in code, developers are strongly urged to |
154 away, because when checking in new code, developers are strongly urged to |
156 test against Isabelle's code base. If your project is part of that code base, |
155 test it against Isabelle's code base. If your project is part of that code base, |
157 then maintenance is done by others. Unfortunately, this might not |
156 then maintenance is done by others. Unfortunately, this might not |
158 be a helpful advice for all types of projects. A lower threshold for inclusion has the |
157 be a helpful advice for all types of projects. A lower threshold for inclusion has the |
159 Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} |
158 Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}} |
160 This archive has been created mainly for formalisations that are |
159 This archive has been created mainly for formalisations that are |
161 interesting but not necessarily of general interest. If you have ML-code as |
160 interesting but not necessarily of general interest. If you have ML-code as |
163 is no problem with updating your code after submission. At the moment |
162 is no problem with updating your code after submission. At the moment |
164 developers are not as diligent with checking their code against the AFP than |
163 developers are not as diligent with checking their code against the AFP than |
165 with checking agains the distribution, but generally problems will be caught |
164 with checking agains the distribution, but generally problems will be caught |
166 and the developer, who caused them, is expected to fix them. So also |
165 and the developer, who caused them, is expected to fix them. So also |
167 in this case code maintenance is done for you. |
166 in this case code maintenance is done for you. |
|
167 |
168 *} |
168 *} |
169 |
169 |
170 section {* Some Naming Conventions in the Isabelle Sources *} |
170 section {* Some Naming Conventions in the Isabelle Sources *} |
171 |
171 |
172 text {* |
172 text {* |