equal
deleted
inserted
replaced
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 |
47 were written on the ML-level. Many parts of this manual are outdated |
47 were written on the ML-level. Many parts of this manual are outdated |
48 now, but some parts, particularly the chapters on tactics, are still |
48 now, but some parts, particularly the chapters on tactics, are still |
49 useful. |
49 useful. |
50 |
50 |
51 \item[The Isar Reference Manual] is also an older document that provides |
51 \item[The Isar Reference Manual] provides specification material (like grammars, |
52 material about Isar and its implementation. Some material in it |
52 examples and so on) about Isar and its implementation. It is currently in |
53 is still useful. |
53 the process of being updated. . |
54 \end{description} |
54 \end{description} |
55 |
55 |
56 Then of course there is: |
56 Then of course there is: |
57 |
57 |
58 \begin{description} |
58 \begin{description} |
134 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
134 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
135 chapter and also contributed the material on @{text NamedThmsFun}. |
135 chapter and also contributed the material on @{text NamedThmsFun}. |
136 \end{itemize} |
136 \end{itemize} |
137 |
137 |
138 Please let me know of any omissions. Responsibility for any remaining |
138 Please let me know of any omissions. Responsibility for any remaining |
139 errors lies with me. |
139 errors lies with me.\bigskip |
|
140 |
|
141 {\Large\bf |
|
142 This document is still in the process of being written! All of the |
|
143 text is still under constructions. Sections and |
|
144 chapters that are under \underline{heavy} construction are marked |
|
145 with TBD.} |
|
146 |
|
147 |
|
148 \vfill |
|
149 This document was compiled with:\\ |
|
150 \input{version} |
140 *} |
151 *} |
141 |
152 |
|
153 |
|
154 |
142 end |
155 end |