89 other hand, Isabelle/Isar comes much closer to existing mathematical practice |
89 other hand, Isabelle/Isar comes much closer to existing mathematical practice |
90 of formal proof, so users with less experience in old-style tactical proving, |
90 of formal proof, so users with less experience in old-style tactical proving, |
91 but a good understanding of mathematical proof might cope with Isar even |
91 but a good understanding of mathematical proof might cope with Isar even |
92 better. |
92 better. |
93 |
93 |
94 Unfortunately, there is no tutorial on Isabelle/Isar available yet. This |
94 This document really is a \emph{reference manual}. Nevertheless, we will give |
95 document really is a \emph{reference manual}. Nevertheless, we will give some |
95 some discussions of the general principles underlying Isar in |
96 discussions of the general principles underlying Isar in |
|
97 chapter~\ref{ch:basics}, and provide some clues of how these may be put into |
96 chapter~\ref{ch:basics}, and provide some clues of how these may be put into |
98 practice. Some more background information on Isar is given in |
97 practice. Some more background information on Isar is given in |
99 \cite{Wenzel:1999:TPHOL}. Furthermore, there are several examples distributed |
98 \cite{Wenzel:1999:TPHOL}. While there is no proper tutorial on Isabelle/Isar |
100 with Isabelle (see directory \texttt{HOL/Isar_examples}). |
99 available yet, there are several examples distributed with Isabelle. See |
|
100 \texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the |
|
101 Isabelle library: |
101 |
102 |
|
103 \begin{center}\small |
|
104 \begin{tabular}{l} |
|
105 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
|
106 \url{http://isabelle.in.tum.de/library/} \\ |
|
107 \end{tabular} |
|
108 \end{center} |
|
109 |
|
110 Apart from browsable HTML sources, both example sessions also provide actual |
|
111 documents. |
102 |
112 |
103 %%% Local Variables: |
113 %%% Local Variables: |
104 %%% mode: latex |
114 %%% mode: latex |
105 %%% TeX-master: "isar-ref" |
115 %%% TeX-master: "isar-ref" |
106 %%% End: |
116 %%% End: |