1 <?xml version='1.0' encoding='iso-8859-1' ?> |
|
2 <!DOCTYPE table PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
3 <!-- $Id$ --> |
|
4 <table class="download"> |
|
5 <tr><td colspan="3" class="downloadheader">Isabelle</td></tr> |
|
6 <tr> |
|
7 <td> |
|
8 Sources and documentation |
|
9 </td> |
|
10 <?downloadCells target="//dist/Isabelle2005.tar.gz" title="Isabelle2005.tar.gz"?> |
|
11 </tr> |
|
12 <tr> |
|
13 <td> |
|
14 Documentation in PDF |
|
15 </td> |
|
16 <?downloadCells target="//dist/Isabelle2005_pdf.tar.gz" title="Isabelle2005_pdf.tar.gz"?> |
|
17 </tr> |
|
18 <tr> |
|
19 <td> |
|
20 Theory library in PDF and HTML |
|
21 </td> |
|
22 <?downloadCells target="//dist/Isabelle2005_library.tar.gz" title="Isabelle2005_library.tar.gz"?> |
|
23 </tr> |
|
24 <tr><td colspan="3" class="downloadheader">Proof General</td></tr> |
|
25 <tr> |
|
26 <td> |
|
27 Proof General |
|
28 </td> |
|
29 <?downloadCells target="//dist/contrib/ProofGeneral.tar.gz" title="ProofGeneral.tar.gz"?> |
|
30 </tr> |
|
31 <tr><td colspan="3" class="downloadheader">Poly/ML compiler and runtime system</td></tr> |
|
32 <tr> |
|
33 <td rowspan="3"> |
|
34 Poly/ML |
|
35 </td> |
|
36 <?downloadCells target="//dist/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?> |
|
37 </tr> |
|
38 <tr class="rowspan"> |
|
39 <?downloadCells target="//dist/contrib/polyml_sparc-solaris.tar.gz" title="polyml_sparc-solaris.tar.gz"?> |
|
40 </tr> |
|
41 <tr class="rowspan"> |
|
42 <?downloadCells target="//dist/contrib/polyml_ppc-darwin.tar.gz" title="polyml_ppc-darwin.tar.gz"?> |
|
43 </tr> |
|
44 <tr><td colspan="3" class="downloadheader">Precompiled logics</td></tr> |
|
45 <tr> |
|
46 <td rowspan="3"> |
|
47 HOL |
|
48 </td> |
|
49 <?downloadCells target="//dist/HOL_x86-linux.tar.gz" title="HOL_x86-linux.tar.gz"?> |
|
50 </tr> |
|
51 <tr class="rowspan"> |
|
52 <?downloadCells target="//dist/HOL_sparc-solaris.tar.gz" title="HOL_sparc-solaris.tar.gz"?> |
|
53 </tr> |
|
54 <tr class="rowspan"> |
|
55 <?downloadCells target="//dist/HOL_ppc-darwin.tar.gz" title="HOL_ppc-darwin.tar.gz"?> |
|
56 </tr> |
|
57 <tr> |
|
58 <td rowspan="3"> |
|
59 HOL-Complex |
|
60 </td> |
|
61 <?downloadCells target="//dist/HOL-Complex_x86-linux.tar.gz" title="HOL-Complex_x86-linux.tar.gz"?> |
|
62 </tr> |
|
63 <tr class="rowspan"> |
|
64 <?downloadCells target="//dist/HOL-Complex_sparc-solaris.tar.gz" title="HOL-Complex_sparc-solaris.tar.gz"?> |
|
65 </tr> |
|
66 <tr class="rowspan"> |
|
67 <?downloadCells target="//dist/HOL-Complex_ppc-darwin.tar.gz" title="HOL-Complex_ppc-darwin.tar.gz"?> |
|
68 </tr> |
|
69 <tr> |
|
70 <td rowspan="3"> |
|
71 HOL4 |
|
72 </td> |
|
73 <?downloadCells target="//dist/HOL4_x86-linux.tar.gz" title="HOL4_x86-linux.tar.gz"?> |
|
74 </tr> |
|
75 <tr class="rowspan"> |
|
76 <?downloadCells target="//dist/HOL4_sparc-solaris.tar.gz" title="HOL4_sparc-solaris.tar.gz"?> |
|
77 </tr> |
|
78 <tr class="rowspan"> |
|
79 <?downloadCells target="//dist/HOL4_ppc-darwin.tar.gz" title="HOL4_ppc-darwin.tar.gz"?> |
|
80 </tr> |
|
81 <tr> |
|
82 <td rowspan="3"> |
|
83 ZF |
|
84 </td> |
|
85 <?downloadCells target="//dist/ZF_x86-linux.tar.gz" title="ZF_x86-linux.tar.gz"?> |
|
86 </tr> |
|
87 <tr class="rowspan"> |
|
88 <?downloadCells target="//dist/ZF_sparc-solaris.tar.gz" title="ZF_sparc-solaris.tar.gz"?> |
|
89 </tr> |
|
90 <tr class="rowspan"> |
|
91 <?downloadCells target="//dist/ZF_ppc-darwin.tar.gz" title="ZF_ppc-darwin.tar.gz"?> |
|
92 </tr> |
|
93 <tr><td colspan="3" class="downloadheader">HOL4 proof terms</td></tr> |
|
94 <tr> |
|
95 <td> |
|
96 HOL4 proof terms |
|
97 </td> |
|
98 <?downloadCells target="//dist/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?> |
|
99 </tr> |
|
100 </table> |
|