|
15585
|
1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
|
2 |
|
|
|
3 |
<!-- $Id$ -->
|
|
|
4 |
|
|
8810
|
5 |
<html>
|
|
|
6 |
|
|
15585
|
7 |
<head>
|
|
|
8 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
|
|
|
9 |
<title>The Isabelle Library ({ISABELLE})</title>
|
|
|
10 |
</head>
|
|
8810
|
11 |
|
|
|
12 |
<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
|
|
|
13 |
|
|
|
14 |
<center>
|
|
|
15 |
<table width="100%" border="0" cellspacing="10" cellpadding="0">
|
|
|
16 |
<tr>
|
|
|
17 |
<td width="20%" valign="middle" align="center">
|
|
|
18 |
<img align=bottom src="isabelle.gif" width="100" height="86" alt="[Isabelle]">
|
|
|
19 |
</td>
|
|
|
20 |
<td width="80%" valign="middle" align="center">
|
|
|
21 |
<table width="90%" border="0" cellspacing="0" cellpadding="20">
|
|
|
22 |
<tr>
|
|
|
23 |
<td valign="middle" align="center" bgcolor="#aacccc">
|
|
|
24 |
<font face="Helvetica,Arial" size="+2">The Isabelle Library</font>
|
|
|
25 |
</td>
|
|
|
26 |
</tr>
|
|
|
27 |
</table>
|
|
|
28 |
</td>
|
|
|
29 |
</tr>
|
|
|
30 |
</table>
|
|
|
31 |
</center>
|
|
|
32 |
|
|
|
33 |
<hr>
|
|
|
34 |
|
|
|
35 |
Higher-Order Logic
|
|
|
36 |
|
|
|
37 |
<ul>
|
|
14639
|
38 |
<li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
|
|
8810
|
39 |
<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
|
|
|
40 |
</ul>
|
|
|
41 |
|
|
|
42 |
<hr>
|
|
|
43 |
|
|
|
44 |
First-Order Logic
|
|
|
45 |
|
|
|
46 |
<ul>
|
|
|
47 |
<li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
|
|
|
48 |
<li><a href="ZF/index.html">ZF (Set Theory)</a>
|
|
|
49 |
<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
|
|
|
50 |
<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
|
|
|
51 |
<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
|
|
|
52 |
</ul>
|
|
|
53 |
|
|
|
54 |
<hr>
|
|
|
55 |
|
|
|
56 |
Miscellaneous
|
|
|
57 |
|
|
|
58 |
<ul>
|
|
|
59 |
<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
|
|
|
60 |
<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
|
|
|
61 |
<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
|
|
|
62 |
</ul>
|
|
|
63 |
|
|
|
64 |
<hr>
|
|
|
65 |
|
|
|
66 |
</body>
|
|
|
67 |
</html>
|