lib/html/index.html
author wenzelm
Wed, 26 Jul 2006 00:44:44 +0200
changeset 20207 4c57e850e8d5
parent 15585 513aa9a3a26d
child 25232 9b4d0c13c332
permissions -rw-r--r--
added Pure/subgoal.ML;

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<!-- $Id$ -->

<html>

<head>
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <title>The Isabelle Library ({ISABELLE})</title>
</head>

<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">

<center>
  <table width="100%" border="0" cellspacing="10" cellpadding="0">
    <tr>
      <td width="20%" valign="middle" align="center">
        <img align=bottom src="isabelle.gif" width="100" height="86" alt="[Isabelle]">
      </td>
      <td width="80%" valign="middle" align="center">
        <table width="90%" border="0" cellspacing="0" cellpadding="20">
          <tr>
            <td valign="middle" align="center" bgcolor="#aacccc">
              <font face="Helvetica,Arial" size="+2">The Isabelle Library</font>
            </td>
          </tr>
        </table>
      </td>
    </tr>
  </table>
</center>

<hr>

Higher-Order Logic

<ul>
<li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
</ul>

<hr>

First-Order Logic

<ul>
<li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
<li><a href="ZF/index.html">ZF (Set Theory)</a>
<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
</ul>

<hr>

Miscellaneous

<ul>
<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
</ul>

<hr>

</body>
</html>