102 Isabelle is still under development. Projects under consideration include |
102 Isabelle is still under development. Projects under consideration include |
103 better support for inductive definitions, some means of recording proofs, a |
103 better support for inductive definitions, some means of recording proofs, a |
104 graphical user interface, and developments in the standard object-logics. |
104 graphical user interface, and developments in the standard object-logics. |
105 I hope but cannot promise to maintain upwards compatibility. |
105 I hope but cannot promise to maintain upwards compatibility. |
106 |
106 |
107 Isabelle is available by anonymous ftp: |
107 Isabelle can be downloaded from . |
108 \begin{itemize} |
108 \begin{quote} |
109 \item University of Cambridge\\ |
109 {\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/} |
110 host {\tt ftp.cl.cam.ac.uk}\\ |
110 \end{quote} |
111 directory {\tt ml} |
|
112 |
|
113 \item Technical University of Munich\\ |
|
114 host {\tt ftp.informatik.tu-muenchen.de}\\ |
|
115 directory {\tt local/lehrstuhl/nipkow} |
|
116 \end{itemize} |
|
117 The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk} |
111 The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk} |
118 provides a forum for discussing problems and applications involving |
112 provides a forum for discussing problems and applications involving |
119 Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}. |
113 Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}. |
120 Please notify me of any errors you find in this book. |
114 Please notify me of any errors you find in this book. |
121 |
115 |