author haftmann
Tue, 30 Oct 2007 10:30:09 +0100
changeset 25232 9b4d0c13c332
parent 15585 513aa9a3a26d
child 25233 9146551357f6
permissions -rw-r--r--
tidied version

<?xml version="1.0" encoding="iso-8859-1"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
<!-- $Id$ -->

<html xmlns="">
  <meta name="generator" content="HTML Tidy for Linux/x86 (vers 31 October 2006), see" />
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />

  <title>The Isabelle Library ({ISABELLE})</title>

<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
    <table width="100%" border="0" cellspacing="10" cellpadding="0">
        <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">
              <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">The Isabelle Library</font></td>
  <hr />
  Higher-Order Logic

    <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li>

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

    <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a></li>

    <li><a href="ZF/index.html">ZF (Set Theory)</a></li>

    <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>

    <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>

    <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
  <hr />

    <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>

    <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a></li>

    <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
  <hr />