6 <html xmlns="http://www.w3.org/1999/xhtml"> |
6 <html xmlns="http://www.w3.org/1999/xhtml"> |
7 <head> |
7 <head> |
8 <meta name="generator" content="HTML Tidy for Linux/x86 (vers 31 October 2006), see www.w3.org" /> |
8 <meta name="generator" content="HTML Tidy for Linux/x86 (vers 31 October 2006), see www.w3.org" /> |
9 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> |
9 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> |
10 |
10 |
11 <title>The Isabelle Library ({ISABELLE})</title> |
11 <title>The {ISABELLE} Library</title> |
12 </head> |
12 </head> |
13 |
13 |
14 <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040"> |
14 <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040"> |
15 <center> |
15 <center> |
16 <table width="100%" border="0" cellspacing="10" cellpadding="0"> |
16 <table width="100%" border="0" cellspacing="10" cellpadding="0"> |
17 <tr> |
17 <tr> |
18 <td width="20%" valign="middle" align="center"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" /></td> |
18 <td width="20%" valign="middle" align="center"><a href="http://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td> |
19 |
19 |
20 <td width="80%" valign="middle" align="center"> |
20 <td width="80%" valign="middle" align="center"> |
21 <table width="90%" border="0" cellspacing="0" cellpadding="20"> |
21 <table width="90%" border="0" cellspacing="0" cellpadding="20"> |
22 <tr> |
22 <tr> |
23 <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">The Isabelle Library</font></td> |
23 <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">The {ISABELLE} Library</font></td> |
24 </tr> |
24 </tr> |
25 </table> |
25 </table> |
26 </td> |
26 </td> |
27 </tr> |
27 </tr> |
28 </table> |
28 </table> |
29 </center> |
29 </center> |
30 <hr /> |
30 <hr /> |
31 Higher-Order Logic |
|
32 |
31 |
33 <ul> |
32 <ul> |
34 <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li> |
33 <li>Higher-Order Logic</li> |
35 |
34 |
36 <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a></li> |
35 <li style="list-style: none"> |
|
36 <ul> |
|
37 <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li> |
|
38 |
|
39 <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a></li> |
|
40 </ul> |
|
41 </li> |
37 </ul> |
42 </ul> |
38 <hr /> |
|
39 First-Order Logic |
|
40 |
43 |
41 <ul> |
44 <ul> |
42 <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a></li> |
45 <li>First-Order Logic</li> |
43 |
46 |
44 <li><a href="ZF/index.html">ZF (Set Theory)</a></li> |
47 <li style="list-style: none"> |
|
48 <ul> |
|
49 <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a></li> |
45 |
50 |
46 <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li> |
51 <li><a href="ZF/index.html">ZF (Set Theory)</a></li> |
47 |
52 |
48 <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li> |
53 <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li> |
49 |
54 |
50 <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li> |
55 <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li> |
|
56 |
|
57 <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li> |
|
58 </ul> |
|
59 </li> |
51 </ul> |
60 </ul> |
52 <hr /> |
|
53 Miscellaneous |
|
54 |
61 |
55 <ul> |
62 <ul> |
56 <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li> |
63 <li>Miscellaneous</li> |
57 |
64 |
58 <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a></li> |
65 <li style="list-style: none"> |
|
66 <ul> |
|
67 <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li> |
59 |
68 |
60 <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li> |
69 <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a></li> |
|
70 |
|
71 <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li> |
|
72 </ul> |
|
73 </li> |
61 </ul> |
74 </ul> |
62 <hr /> |
|
63 </body> |
75 </body> |
64 </html> |
76 </html> |