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

<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<title>Index of Isabelle/ZF (Isabelle2005: October 2005)</title>
<link rel="stylesheet" type="text/css" href="isabelle.css">
</head>

<body>
<div class="head"><h1>Index of Isabelle/ZF</h1>

<p><a href="../index.html">Up</a> to index of Isabelle</p>

<p>View <a href="medium.html">theory dependencies</a><br>
View <a href="README.html">README</a><br>
View <a href="document.pdf">document</a><br>
View <a href="outline.pdf">outline</a></p>

</div>
<hr>
<div class="theories">
<h2>Theories</h2>
<ul>
<li><a href="ZF.html">ZF</a>
<li><a href="upair.html">upair</a>
<li><a href="pair.html">pair</a>
<li><a href="equalities.html">equalities</a>
<li><a href="Fixedpt.html">Fixedpt</a>
<li><a href="Bool.html">Bool</a>
<li><a href="Sum.html">Sum</a>
<li><a href="func.html">func</a>
<li><a href="QPair.html">QPair</a>
<li><a href="Inductive.html">Inductive</a>
<li><a href="Perm.html">Perm</a>
<li><a href="Trancl.html">Trancl</a>
<li><a href="WF.html">WF</a>
<li><a href="Ordinal.html">Ordinal</a>
<li><a href="OrdQuant.html">OrdQuant</a>
<li><a href="Nat.html">Nat</a>
<li><a href="Epsilon.html">Epsilon</a>
<li><a href="Order.html">Order</a>
<li><a href="OrderArith.html">OrderArith</a>
<li><a href="OrderType.html">OrderType</a>
<li><a href="Finite.html">Finite</a>
<li><a href="Cardinal.html">Cardinal</a>
<li><a href="Univ.html">Univ</a>
<li><a href="QUniv.html">QUniv</a>
<li><a href="Datatype.html">Datatype</a>
<li><a href="Arith.html">Arith</a>
<li><a href="ArithSimp.html">ArithSimp</a>
<li><a href="List.html">List</a>
<li><a href="EquivClass.html">EquivClass</a>
<li><a href="Int.html">Int</a>
<li><a href="Bin.html">Bin</a>
<li><a href="IntArith.html">IntArith</a>
<li><a href="IntDiv.html">IntDiv</a>
<li><a href="CardinalArith.html">CardinalArith</a>
<li><a href="Main.html">Main</a>
<li><a href="AC.html">AC</a>
<li><a href="Zorn.html">Zorn</a>
<li><a href="Cardinal_AC.html">Cardinal_AC</a>
<li><a href="InfDatatype.html">InfDatatype</a>
<li><a href="Main_ZFC.html">Main_ZFC</a>
