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