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