refurbished some old README.html files as session descriptions, which show up in chapter index;
authorwenzelm
Tue, 12 Mar 2013 21:59:48 +0100
changeset 51403 2ff3a5589b05
parent 51402 b05cd411d3d3
child 51404 90a598019aeb
refurbished some old README.html files as session descriptions, which show up in chapter index;
src/CTT/README.html
src/CTT/ROOT
src/Cube/README.html
src/Cube/ROOT
src/FOL/README.html
src/FOL/ROOT
src/HOL/HOLCF/FOCUS/README.html
src/HOL/HOLCF/IMP/README.html
src/HOL/HOLCF/IOA/README.html
src/HOL/Hahn_Banach/README.html
src/HOL/IMPP/README.html
src/HOL/IOA/README.html
src/HOL/Induct/README.html
src/HOL/Isar_Examples/README.html
src/HOL/Prolog/README.html
src/HOL/Proofs/Lambda/README.html
src/HOL/README.html
src/HOL/ROOT
src/LCF/README.html
src/LCF/ROOT
src/Sequents/README.html
src/Sequents/ROOT
src/ZF/AC/README.html
src/ZF/Coind/README.html
src/ZF/Constructible/README.html
src/ZF/IMP/README.html
src/ZF/README.html
src/ZF/ROOT
src/ZF/Resid/README.html
src/ZF/ex/README.html
--- a/src/CTT/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-<!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>CTT/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>CTT: Constructive Type Theory</H2>
-
-This is a version of Constructive Type Theory (extensional equality, no universes).<p>
-
-Useful references on Constructive Type Theory:
-
-<UL>
-<LI>	B. Nordstr÷m, K. Petersson and J. M. Smith,<BR>
-	Programming in Martin-L÷f's Type Theory<BR>
-	(Oxford University Press, 1990)
-
-<LI>	Simon Thompson,<BR>
-	Type Theory and Functional Programming (Addison-Wesley, 1991)
-</UL>
-
-</BODY>
-</HTML>
--- a/src/CTT/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/CTT/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -4,6 +4,17 @@
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
+
+    This is a version of Constructive Type Theory (extensional equality,
+    no universes).
+
+    Useful references on Constructive Type Theory:
+
+    B. Nordstr├Âm, K. Petersson and J. M. Smith, Programming in Martin-L├Âf's
+    Type Theory (Oxford University Press, 1990)
+
+    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
+    1991)
   *}
   options [document = false]
   theories Main
--- a/src/Cube/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<!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>Cube/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Cube: Barendregt's Lambda-Cube</H2>
-
-This directory contains the theory sources for the Lambda-Cube in
-Isabelle/Pure.<p>
-
-The <tt>ex</tt> subdirectory contains some examples.<p>
-
-NB: the formalization is not completely sound!  It does not enforce
-distinctness of variable names in contexts!<P>
-
-For more information about the Lambda-Cube, see
-
-<UL>
-<LI>H. Barendregt<BR>
-    Introduction to Generalised Type Systems<BR>
-    J. Functional Programming
-</UL>
-</BODY>
-</HTML>
--- a/src/Cube/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/Cube/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -5,7 +5,13 @@
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
-    The Lambda-Cube a la Barendregt.
+    Barendregt's Lambda-Cube.
+
+    NB: the formalization is not completely sound!  It does not enforce
+    distinctness of variable names in contexts!
+
+    For more information about the Lambda-Cube, see H. Barendregt, Introduction
+    to Generalised Type Systems, J. Functional Programming.
   *}
   options [document = false]
   theories Example
--- a/src/FOL/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<!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>FOL/README</title>
-</head>
-
-<body>
-
-<h2>FOL: First-Order Logic with Natural Deduction</h2>
-
-This directory contains the ML sources of the Isabelle system for
-First-Order Logic (constructive and classical versions).  For a
-classical sequent calculus, see LK.<p>
-
-The <tt>ex</tt> subdirectory contains some examples.<p>
-
-Useful references on First-Order Logic:
-
-<ul>
-<li>Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br>
-(The first chapter is an excellent introduction to natural
-deduction in general.)
-<li>Antony Galton, Logic for Information Technology (Wiley, 1990)
-<li>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
-</ul>
-</body>
-</html>
--- a/src/FOL/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/FOL/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -1,12 +1,28 @@
 chapter FOL
 
 session FOL = Pure +
-  description "First-Order Logic with Natural Deduction"
+  description {*
+    First-Order Logic with Natural Deduction (constructive and classical
+    versions). For a classical sequent calculus, see Isabelle/LK.
+
+    Useful references on First-Order Logic:
+
+    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
+    1991) (The first chapter is an excellent introduction to natural deduction
+    in general.)
+
+    Antony Galton, Logic for Information Technology (Wiley, 1990)
+
+    Michael Dummett, Elements of Intuitionism (Oxford, 1977)
+  *}
   options [proofs = 2]
   theories FOL
   files "document/root.tex"
 
 session "FOL-ex" in ex = FOL +
+  description {*
+    Examples for First-Order Logic.
+  *}
   theories
     First_Order_Logic
     Natural_Numbers
--- a/src/HOL/HOLCF/FOCUS/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-<!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>HOLCF/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H3>FOCUS: a theory of stream-processing functions Isabelle/<A HREF="..">HOLCF</A></H3>
-
-For introductions to FOCUSs, see 
-<UL>
-<LI><A HREF="http://www4.in.tum.de/publ/html.php?e=2">The Design of Distributed Systems - An Introduction to FOCUS</A>
-<LI><A HREF="http://www4.in.tum.de/publ/html.php?e=15">Specification and Refinement of a Buffer of Length One</A>
-<LI><A HREF="http://www4.in.tum.de/publ/html.php?e=321">Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement</A>
-</UL>
-For slides on <A HREF="Buffer.html">Buffer.thy</A>, see <A HREF="http://isabelle.in.tum.de/HOLCF/1-Buffer.ps.gz">Coinduction beats induction on streams</A>.
-
-</BODY></HTML>
--- a/src/HOL/HOLCF/IMP/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-<!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>HOLCF/IMP/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>IMP -- A <KBD>WHILE</KBD>-language and its Semantics</H2>
-
-This is the HOLCF-based denotational semantics of a simple
-<tt>WHILE</tt>-language.  For a full description see <A
-HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
-</BODY>
-</HTML>
--- a/src/HOL/HOLCF/IOA/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-<!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>HOLCF/IOA/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H3>IOA: A formalization of I/O automata in HOLCF</H3>
-
-Author:     Olaf M&uuml;ller<BR>
-Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
-
-The distribution contains simulation relations, temporal logic, and an abstraction theory.
-Everything is based upon a domain-theoretic model of finite and infinite sequences. 
-<p>
-For details see the <A HREF="http://www4.informatik.tu-muenchen.de/~isabelle/IOA/">IOA project</a>.
-
-</BODY></HTML>
-
-
--- a/src/HOL/Hahn_Banach/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-<!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>HOL/Hahn_Banach/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
-
-Author: Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
-
-This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
-following H. Heuser, Funktionalanalysis, p. 228 -232.
-The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis.
-It is a conclusion of Zorn's lemma.<P>
-
-Two different formaulations of the theorem are presented, one for general real vectorspaces
-and its application to normed vectorspaces. <P>
-
-The theorem says, that every continous linearform, defined on arbitrary subspaces
-(not only one-dimensional subspaces), can be extended to a continous linearform on
-the whole vectorspace.
-
-
-<HR>
-
-<ADDRESS>
-<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
-</ADDRESS>
-
-</BODY>
-</HTML>
--- a/src/HOL/IMPP/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-<!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>HOL/IMPP/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>IMPP--An imperative language with procedures</H2>
-
-This is an extension of <A HREF="../IMP/">IMP</A> with local variables
-and mutually recursive procedures. For documentation see
-<A HREF="http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html">
-Hoare Logic for Mutual Recursion and Local Variables</A>.
-
-</BODY></HTML>
--- a/src/HOL/IOA/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-<!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>HOLCF/IOA/README</title>
-</head>
-
-<body>
-
-<h3>IOA: A basic formalization of I/O automata in HOL</h3>
-
-Author:     Konrad Slind, Tobias Nipkow and Olaf M&uuml;ller<br>
-Copyright   1995,1996 Technische Universit&auml;t M&uuml;nchen
-
-<p>
-
-This directory contains a formalization of the meta theory of I/O automata in HOL.
-This formalization has been significantly changed and extended.  The new version
-is available in the subdirectory HOLCF/IOA.  There are also the proofs of two
-communication protocols which formerly have been here.
-
-</body>
-</html>
--- a/src/HOL/Induct/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-<!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>HOL/Induct/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Induct--Examples of (Co)Inductive Definitions</H2>
-
-<P>This directory is a collection of small examples to demonstrate
-Isabelle/HOL's (co)inductive definitions package.  Large examples appear on
-many other directories, such as Auth, IMP and Lambda.
-
-<UL>
-
-<LI><KBD>Comb</KBD> proves the Church-Rosser theorem for combinators (<A
-HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz">paper
-available</A>).
-
-<LI><KBD>Mutil</KBD> is the famous Mutilated Chess Board problem (<A
-HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz">paper
-available</A>).
-
-<LI><KBD>PropLog</KBD> proves the completeness of a formalization of
-propositional logic (<A
-HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">paper
-available</A>).
-
-<LI><KBD>Exp</KBD> demonstrates the use of iterated inductive definitions to
-reason about mutually recursive relations.
-</UL>
-
-<HR>
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY></HTML>
--- a/src/HOL/Isar_Examples/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-<!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>HOL/Isar_Examples</title>
-</head>
-
-<body>
-<h1>HOL/Isar_Examples</h1>
-
-Isar offers a new high-level proof (and theory) language interface to
-Isabelle.  This directory contains some example Isar documents.  See
-also the included document, or the <a
-href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more
-information.
-</body>
-</html>
--- a/src/HOL/Prolog/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-<!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>HOL/Prolog/README</TITLE>
-</HEAD>
-
-<BODY>
-<H2>Prolog -- A bare-bones implementation of Lambda-Prolog</H2>
-
-This is a simple exploratory implementation of 
-<A HREF="http://www.cse.psu.edu/~dale/lProlog/">Lambda-Prolog</A> in HOL,
-including some minimal examples (in Test.thy) and a more typical example
-of a little functional language and its type system.
-</BODY>
-</HTML>
--- a/src/HOL/Proofs/Lambda/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-<!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>HOL/Lambda</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Lambda Calculus in de Bruijn's Notation</H1>
-
-This theory defines lambda-calculus terms with de Bruijn indixes and proves
-confluence of beta, eta and  beta+eta.
-<P>
-
-
-The paper
-<A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html">
-More Church-Rosser Proofs (in Isabelle/HOL)</A>
-describes the whole theory.
-
-<HR>
-
-<P>Last modified 20.5.2000
-
-</BODY>
-</HTML>
--- a/src/HOL/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-<!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>HOL/README</title>
-</head>
-
-<body>
-
-<h2>HOL: Higher-Order Logic</h2>
-
-These are the main sources of the Isabelle system for Higher-Order Logic.
-
-<p>
-
-There are also several example sessions:
-<dl>
-
-<dt>Algebra
-<dd>rings and univariate polynomials
-
-<dt>Auth
-<dd>a new approach to verifying authentication protocols
-
-<dt>AxClasses
-<dd>a few basic examples of using axiomatic type classes
-
-<dt>Complex
-<dd>a development of the complex numbers, the reals, and the hyper-reals,
-which are used in non-standard analysis (builds the image HOL-Complex)
-
-<dt>Hoare
-<dd>verification of imperative programs (verification conditions are
-generated automatically from pre/post conditions and loop invariants)
-
-<dt>HoareParallel
-<dd>verification of shared-variable imperative programs a la Owicki-Gries.
-(verification conditions are generated automatically)
-
-<dt>Hyperreal
-<dd>Nonstandard analysis. Builds on Real and is part of Complex.
-
-<dt>IMP
-<dd>mechanization of a large part of a semantics text by Glynn Winskel
-
-<dt>IMPP
-<dd>extension of IMP with local variables and mutually recursive
-procedures
-
-<dt>Import
-<dd>theories imported from other (HOL) theorem provers.
-
-<dt>Induct
-<dd>examples of (co)inductive definitions
-
-<dt>IOA
-<dd>a simple theory of Input/Output Automata
-
-<dt>Isar_Examples
-<dd>several introductory examples using Isabelle/Isar
-
-<dt>Lambda
-<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
-
-<dt>Lattice
-<dd>lattices and order structures (in Isabelle/Isar)
-
-<dt>Library
-<dd>A collection of generic theories
-
-<dt>Matrix
-<dd>two-dimensional matrices
-
-<dt>MicroJava
-<dd>formalization of a fragment of Java, together with a corresponding
-virtual machine and a specification of its bytecode verifier and a
-lightweight bytecode verifier, including proofs of type-safety
-
-<dt>Modelcheck
-<dd>basic setup for integration of some model checkers in Isabelle/HOL
-
-<dt>NanoJava
-<dd>Haore Logic for a tiny fragment of Java
-
-<dt>NumberTheory
-<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
-Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
-
-<dt>Prolog
-<dd>a (bare-bones) implementation of Lambda-Prolog
-
-<dt>Real
-<dd>the real numbers, part of Complex
-
-<dt>Hahn_Banach
-<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
-
-<dt>SET_Protocol
-<dd>verification of the SET Protocol
-
-<dt>Subst
-<dd>a theory of substitution and unification.
-
-<dt>TLA
-<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
-
-<dt>UNITY
-<dd>Chandy and Misra's UNITY formalism
-
-<dt>W0
-<dd>a precursor of MiniML, without let-expressions
-
-<dt>ex
-<dd>miscellaneous examples
-
-</dl>
-
-</body>
-</html>
--- a/src/HOL/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/HOL/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -50,12 +50,40 @@
     Author:     Gertrud Bauer, TU Munich
 
     The Hahn-Banach theorem for real vector spaces.
+
+    This is the proof of the Hahn-Banach theorem for real vectorspaces,
+    following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
+    theorem is one of the fundamental theorems of functioal analysis. It is a
+    conclusion of Zorn's lemma.
+
+    Two different formaulations of the theorem are presented, one for general
+    real vectorspaces and its application to normed vectorspaces.
+
+    The theorem says, that every continous linearform, defined on arbitrary
+    subspaces (not only one-dimensional subspaces), can be extended to a
+    continous linearform on the whole vectorspace.
   *}
   options [document_graph]
   theories Hahn_Banach
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Induct" in Induct = HOL +
+  description {*
+    Examples of (Co)Inductive Definitions.
+
+    Comb proves the Church-Rosser theorem for combinators (see
+    http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
+
+    Mutil is the famous Mutilated Chess Board problem (see
+    http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
+
+    PropLog proves the completeness of a formalization of propositional logic
+    (see
+    HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
+
+    Exp demonstrates the use of iterated inductive definitions to reason about
+    mutually recursive relations.
+  *}
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -117,6 +145,12 @@
   description {*
     Author:     David von Oheimb
     Copyright   1999 TUM
+
+    IMPP -- An imperative language with procedures.
+
+    This is an extension of IMP with local variables and mutually recursive
+    procedures. For documentation see "Hoare Logic for Mutual Recursion and
+    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   *}
   options [document = false]
   theories EvenOdd
@@ -131,6 +165,10 @@
   theories Number_Theory
 
 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
+  description {*
+    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
+    Theorem, Wilson's Theorem, Quadratic Reciprocity.
+  *}
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Infinite_Set"
@@ -147,10 +185,19 @@
   files "document/root.tex"
 
 session "HOL-Hoare" in Hoare = HOL +
+  description {*
+    Verification of imperative programs (verification conditions are generated
+    automatically from pre/post conditions and loop invariants).
+  *}
+
   theories Hoare
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
+  description {*
+    Verification of shared-variable imperative programs a la Owicki-Gries.
+    (verification conditions are generated automatically).
+  *}
   options [document_graph]
   theories Hoare_Parallel
   files "document/root.bib" "document/root.tex"
@@ -217,6 +264,7 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Auth" in Auth = HOL +
+  description {* A new approach to verifying authentication protocols. *}
   options [document_graph]
   theories
     Auth_Shared
@@ -231,7 +279,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-    Verifying security protocols using UNITY.
+    Verifying security protocols using Chandy and Misra's UNITY formalism.
   *}
   options [document_graph]
   theories
@@ -315,6 +363,15 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
+  description {*
+    Lambda Calculus in de Bruijn's Notation.
+
+    This session defines lambda-calculus terms with de Bruijn indixes and
+    proves confluence of beta, eta and beta+eta.
+
+    The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
+    theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
+  *}
   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
@@ -328,11 +385,22 @@
 session "HOL-Prolog" in Prolog = HOL +
   description {*
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+
+    A bare-bones implementation of Lambda-Prolog.
+
+    This is a simple exploratory implementation of Lambda-Prolog in HOL,
+    including some minimal examples (in Test.thy) and a more typical example of
+    a little functional language and its type system.
   *}
   options [document = false]
   theories Test Type
 
 session "HOL-MicroJava" in MicroJava = HOL +
+  description {*
+    Formalization of a fragment of Java, together with a corresponding virtual
+    machine and a specification of its bytecode verifier and a lightweight
+    bytecode verifier, including proofs of type-safety.
+  *}
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   theories MicroJava
@@ -346,6 +414,9 @@
   theories MicroJava
 
 session "HOL-NanoJava" in NanoJava = HOL +
+  description {*
+    Hoare Logic for a tiny fragment of Java.
+  *}
   options [document_graph]
   theories Example
   files "document/root.bib" "document/root.tex"
@@ -361,10 +432,12 @@
 
 session "HOL-IOA" in IOA = HOL +
   description {*
-    Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1994  TU Muenchen
+    Author:     Tobias Nipkow and Konrad Slind and Olaf M├╝ller
+    Copyright   1994--1996  TU Muenchen
 
-    The meta theory of I/O-Automata.
+    The meta theory of I/O-Automata in HOL. This formalization has been
+    significantly changed and extended, see HOLCF/IOA. There are also the
+    proofs of two communication protocols which formerly have been here.
 
     @inproceedings{Nipkow-Slind-IOA,
     author={Tobias Nipkow and Konrad Slind},
@@ -485,7 +558,9 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +
-  description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
+  description {*
+    Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
+  *}
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Number_Theory/Primes"
@@ -511,18 +586,26 @@
     "document/style.tex"
 
 session "HOL-SET_Protocol" in SET_Protocol = HOL +
+  description {*
+    Verification of the SET Protocol.
+  *}
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   theories SET_Protocol
   files "document/root.tex"
 
 session "HOL-Matrix_LP" in Matrix_LP = HOL +
+  description {*
+    Two-dimensional matrices and linear programming.
+  *}
   options [document_graph]
   theories Cplex
   files "document/root.tex"
 
 session "HOL-TLA" in TLA = HOL +
-  description {* The Temporal Logic of Actions *}
+  description {*
+    Lamport's Temporal Logic of Actions.
+  *}
   options [document = false]
   theories TLA
 
@@ -637,6 +720,7 @@
   files "document/root.tex"
 
 session "HOL-NSA" in NSA = HOL +
+  description {* Nonstandard analysis. *}
   options [document_graph]
   theories Hypercomplex
   files "document/root.tex"
@@ -864,6 +948,11 @@
   theories HOLCF_Library
 
 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
+  description {*
+    IMP -- A WHILE-language and its Semantics.
+
+    This is the HOLCF-based denotational semantics of a simple WHILE-language.
+  *}
   options [document = false]
   theories HoareEx
   files "document/root.tex"
@@ -885,6 +974,20 @@
     Pattern_Match
 
 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
+  description {*
+    FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
+
+    For introductions to FOCUS, see
+
+    "The Design of Distributed Systems - An Introduction to FOCUS"
+    http://www4.in.tum.de/publ/html.php?e=2
+
+    "Specification and Refinement of a Buffer of Length One"
+    http://www4.in.tum.de/publ/html.php?e=15
+
+    "Specification and Development of Interactive Systems: Focus on Streams,
+    Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
+  *}
   options [document = false]
   theories
     Fstreams
@@ -894,8 +997,13 @@
 session IOA in "HOLCF/IOA" = HOLCF +
   description {*
     Author:     Olaf Mueller
+    Copyright   1997 TU M├╝nchen
 
-    Formalization of a semantic model of I/O-Automata.
+    A formalization of I/O automata in HOLCF.
+
+    The distribution contains simulation relations, temporal logic, and an
+    abstraction theory. Everything is based upon a domain-theoretic model of
+    finite and infinite sequences.
   *}
   options [document = false]
   theories "meta_theory/Abstraction"
--- a/src/LCF/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-<!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>LCF/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>LCF: Logic for Computable Functions</H2>
-
-This directory contains the ML sources of the Isabelle system for
-LCF, based on FOL.<p>
-
-The <tt>ex</tt> subdirectory contains some examples.<p>
-
-Useful references on LCF:
-
-<UL>
-<LI>Lawrence C. Paulson,<BR>
-    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
-</UL>
-</BODY></HTML>
--- a/src/LCF/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/LCF/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -4,6 +4,11 @@
   description {*
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
+
+    Logic for Computable Functions.
+
+    Useful references on LCF: Lawrence C. Paulson,
+    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
   *}
   options [document = false]
   theories LCF
--- a/src/Sequents/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-<!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>Sequents/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Sequents: Various Sequent Calculi</H2>
-
-This directory contains the ML sources of the Isabelle system for
-various Sequent, Linear, and Modal Logic.<p>
-
-The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
-<tt>ex/Modal</tt> contain some examples.<p>
-
-Much of the work in Modal logic was done by Martin Coen. Thanks to
-Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
-reorganized the files and supplied Linear Logic. Jacob Frost provided
-some improvements to the syntax of sequents.
-
-<P>Useful references on sequent calculi:
-
-<UL>
-<LI>Steve Reeves and Michael Clarke,<BR>
-    Logic for Computer Science (Addison-Wesley, 1990)
-<LI>G. Takeuti,<BR>
-    Proof Theory (North Holland, 1987)
-</UL>
-
-Useful references on Modal Logics:
-<UL>
-<LI>Melvin C Fitting,<BR>
-    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
-
-<LI>Lincoln A. Wallen,<BR>
-    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
-</UL>
-
-Useful references on Linear Logic:
-<UL>
-<LI>A. S. Troelstra<BR>
-    Lectures on Linear Logic (CSLI, 1992)
-
-<LI>S. Kalvala and V. de Paiva<BR>
-    Linear Logic in Isabelle (in TR 379, University of Cambridge
-				Computer Lab, 1995, ed L. Paulson)
-</UL>
-
-</BODY></HTML>
--- a/src/Sequents/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/Sequents/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -5,7 +5,37 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-    Classical Sequent Calculus based on Pure Isabelle.
+    Various Sequent Calculi for Classical, Linear, and Modal Logic.
+
+    Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev
+    Gore' for supplying the inference system for S43. Sara Kalvala reorganized
+    the files and supplied Linear Logic. Jacob Frost provided some improvements
+    to the syntax of sequents.
+
+
+    Useful references on sequent calculi:
+
+    Steve Reeves and Michael Clarke, Logic for Computer Science
+    (Addison-Wesley, 1990)
+
+    G. Takeuti, Proof Theory (North Holland, 1987)
+
+
+    Useful references on Modal Logics:
+
+    Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics
+    (Reidel, 1983)
+
+    Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press,
+    1990)
+
+
+    Useful references on Linear Logic:
+
+    A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992)
+
+    S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
+    of Cambridge Computer Lab, 1995, ed L. Paulson)
   *}
   options [document = false]
   theories
--- a/src/ZF/AC/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-<!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>ZF/AC/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>AC -- Equivalents of the Axiom of Choice</H2>
-
-Krzysztof Grabczewski has mechanized the first two chapters of the book
-
-<P>
-<PRE>
-@book{rubin&amp;rubin,
-  author	= "Herman Rubin and Jean E. Rubin",
-  title		= "Equivalents of the Axiom of Choice, {II}",
-  publisher	= "North-Holland",
-  year		= 1985}
-</PRE>
-
-<P>
-The report
-<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>,
-by Paulson and Grabczewski, describes both this development and ZF's theories
-of cardinals.
-
-</body>
-</html>
--- a/src/ZF/Coind/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-<!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>ZF/Coind/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Coind -- A Coinduction Example</H2>
-
-Jacob Frost has mechanized the proofs from the article
-
-<P>
-<PRE>
-@Article{milner-coind,
-  author	= "Robin Milner and Mads Tofte",
-  title		= "Co-induction in Relational Semantics",
-  journal	= TCS,
-  year		= 1991,
-  volume	= 87,
-  pages		= "209--220"}
-</PRE>
-
-<P> It involves proving the consistency of the dynamic and static semantics
-for a small functional language.  A codatatype definition specifies values and
-value environments in mutual recursion: non-well-founded values represent
-recursive functions; value environments are variant functions from variables
-into values.
-
-<P>
-Frost's
-<A
-HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
-
-</body>
-</html>
--- a/src/ZF/Constructible/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-<!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>ZF/Constructible/README</title>
-</head>
-
-<body>
-<h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
-
-G&ouml;del's proof of the relative consistency of the axiom of choice is
-mechanized using Isabelle/ZF.  The proof builds upon a previous mechanization
-of the
-<a href="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
-theorem</a>.  The heavy reliance on metatheory in the original proof makes the
-formalization unusually long, and not entirely satisfactory: two parts of the
-proof do not fit together.  It seems impossible to solve these problems
-without formalizing the metatheory.  However, the present development follows
-a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the
-formalization of further material from that book.  It also serves as an
-example of what to expect when deep mathematics is formalized.  
-
-A paper describing this development is
-<a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.
-
-<hr>
-
-<p>
-
-Last modified $Date$
-
-<address>
-<a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
-<a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a>
-</address>
-</body>
-</html>
--- a/src/ZF/IMP/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-<!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>ZF/IMP/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
-
-The formalization of the denotational and operational semantics of a simple
-while-language together with an equivalence proof between the two semantics.
-The whole development essentially formalizes/transcribes chapters 2 and 5 of
-<P>
-<PRE>
-@book{Winskel,
- author = {Glynn Winskel},
- title = {The Formal Semantics of Programming Languages},
- publisher = {MIT Press},
- year = 1993}.
-</PRE>
-<P>
-There is a
-<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">report</A>
-by L&ouml;tzbeyer and Sandner.
-<P>
-A much extended version of this development is found in
-<A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
-</BODY></HTML>
--- a/src/ZF/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-<!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>ZF/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
-
-This directory contains the ML sources of the Isabelle system for
-ZF Set Theory, based on FOL.<p>
-
-There are several subdirectories of examples:
-<DL>
-<DT>AC
-<DD>subdirectory containing proofs from the book "Equivalents of the Axiom
-of Choice, II" by H. Rubin and J.E. Rubin, 1985.  Thanks to Krzysztof
-Gr`abczewski.<P>
-
-<DT>Coind
-<DD>subdirectory containing a large example of proof by co-induction.  It
-is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P>
-
-<DT>IMP
-<DD>subdirectory containing a semantics equivalence proof between
-operational and denotational definitions of a simple programming language.
-Thanks to Heiko Loetzbeyer & Robert Sandner.<P>
-
-<DT>Resid
-<DD>subdirectory containing a proof of the Church-Rosser Theorem.  It is
-by Ole Rasmussen, following the Coq proof by G´┐Żard Huet.<P>
-
-<DT>ex
-<DD>subdirectory containing various examples.
-</DL>
-
-Isabelle/ZF formalizes the greater part of elementary set theory,
-including relations, functions, injections, surjections, ordinals and
-cardinals.  Results proved include Cantor's Theorem, the Recursion
-Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the
-Wellordering Theorem.<P>
-
-Isabelle/ZF also provides theories of lists, trees, etc., for
-formalizing computational notions.  It supports inductive definitions
-of infinite-branching trees for any cardinality of branching.<P>
-
-Useful references for Isabelle/ZF:
-
-<UL>
-<LI>	Lawrence C. Paulson,<BR>
-	Set theory for verification: I. From foundations to functions.<BR>
-	J. Automated Reasoning 11 (1993), 353-389.
-
-<LI>	Lawrence C. Paulson,<BR>
-	Set theory for verification: II. Induction and recursion.<BR>
-	Report 312, Computer Lab (1993).<BR>
-
-<LI>	Lawrence C. Paulson,<BR>
-	A fixedpoint approach to implementing (co)inductive definitions. <BR> 
-	In: A. Bundy (editor),<BR>
-	CADE-12: 12th International Conference on Automated Deduction,<BR>
-	(Springer LNAI 814, 1994), 148-161.
-</UL>
-
-Useful references on ZF set theory:
-
-<UL>
-<LI>	Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
-
-<LI>	Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
-
-<LI>	Keith J. Devlin,<BR>
-	Fundamentals of Contemporary Set Theory (Springer, 1979)
-
-<LI>	Kenneth Kunen<BR>
-	Set Theory: An Introduction to Independence Proofs<BR>
-	(North-Holland, 1980)
-</UL>
-
-</BODY></HTML>
--- a/src/ZF/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/ZF/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -5,9 +5,42 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
-    Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
+    Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
+    Philippe Noel and Lawrence Paulson.
+
+    Isabelle/ZF formalizes the greater part of elementary set theory, including
+    relations, functions, injections, surjections, ordinals and cardinals.
+    Results proved include Cantor's Theorem, the Recursion Theorem, the
+    Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
+
+    Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
+    computational notions. It supports inductive definitions of
+    infinite-branching trees for any cardinality of branching.
+
+
+    Useful references for Isabelle/ZF:
+
+    Lawrence C. Paulson, Set theory for verification: I. From foundations to
+    functions. J. Automated Reasoning 11 (1993), 353-389.
 
-    This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+    Lawrence C. Paulson, Set theory for verification: II. Induction and
+    recursion. Report 312, Computer Lab (1993).
+
+    Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive
+    definitions. In: A. Bundy (editor), CADE-12: 12th International
+    Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161.
+
+
+    Useful references on ZF set theory:
+
+    Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
+
+    Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
+
+    Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979)
+
+    Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
+    (North-Holland, 1980)
   *}
   options [document_graph]
   theories
@@ -21,6 +54,14 @@
     Copyright   1995  University of Cambridge
 
     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
+
+    See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and
+    J.E. Rubin, 1985.
+
+    The report
+    http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
+    "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
+    development and ZF's theories of cardinals.
   *}
   options [document_graph]
   theories
@@ -43,6 +84,12 @@
 
     Coind -- A Coinduction Example.
 
+    It involves proving the consistency of the dynamic and static semantics for
+    a small functional language. A codatatype definition specifies values and
+    value environments in mutual recursion: non-well-founded values represent
+    recursive functions; value environments are variant functions from
+    variables into values.
+
     Based upon the article
         Robin Milner and Mads Tofte,
         Co-induction in Relational Semantics,
@@ -51,12 +98,31 @@
     Written up as
         Jacob Frost, A Case Study of Co_induction in Isabelle
         Report, Computer Lab, University of Cambridge (1995).
+        http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
   *}
   options [document = false]
   theories ECR
 
 session "ZF-Constructible" in Constructible = ZF +
-  description {* Inner Models, Absoluteness and Consistency Proofs. *}
+  description {*
+    Relative Consistency of the Axiom of Choice:
+    Inner Models, Absoluteness and Consistency Proofs.
+
+    G├Âdel's proof of the relative consistency of the axiom of choice is
+    mechanized using Isabelle/ZF. The proof builds upon a previous
+    mechanization of the reflection theorem (see
+    http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy
+    reliance on metatheory in the original proof makes the formalization
+    unusually long, and not entirely satisfactory: two parts of the proof do
+    not fit together. It seems impossible to solve these problems without
+    formalizing the metatheory. However, the present development follows a
+    standard textbook, Kunen's Set Theory, and could support the formalization
+    of further material from that book. It also serves as an example of what to
+    expect when deep mathematics is formalized.
+
+    A paper describing this development is
+    http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
+  *}
   options [document_graph]
   theories DPow_absolute AC_in_L Rank_Separation
   files "document/root.tex" "document/root.bib"
@@ -122,6 +188,10 @@
 
     Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
     J. Functional Programming 4(3) 1994, 371-394.
+
+    See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
+    Porting Experiment.
+    http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   *}
   options [document = false]
   theories Confluence
@@ -150,6 +220,15 @@
     Copyright   1993  University of Cambridge
 
     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
+
+    Includes a simple form of Ramsey's theorem. A report is available:
+    http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
+
+    Several (co)inductive and (co)datatype definitions are presented. The
+    report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
+    describes the theoretical foundations of datatypes while
+    href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
+    describes the package that automates their declaration.
   *}
   options [document = false]
   theories
--- a/src/ZF/Resid/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-<!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>ZF/Resid/README</title>
-</head>
-
-<body>
-
-<h2>Resid -- A theory of residuals</h2>
-
-Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
-article
-
-<p>
-
-<pre>
-@Article{huet-residual,
-  author  = "{G\'erard} Huet",
-  title   = "Residual Theory in $\lambda$-Calculus: A Formal Development",
-  journal = JFP,
-  year    = 1994,
-  volume  = 4,
-  number  = 3,
-  pages   = "371--394"}
-</pre>
-
-See Rasmussen's report <a
-href="http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment</a>.
-
-</body>
-</html>
--- a/src/ZF/ex/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-<!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>ZF/ex/README</title>
-</head>
-
-<body>
-
-<h2>ZF general examples</h2>
-
-Examples on this directory include a simple form of Ramsey's theorem.  A <a href="http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z">report</a> is available.
-
-<p>
-
-Several (co)inductive and (co)datatype definitions are presented.  <a href="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">One report</a> describes the theoretical foundations of datatypes while <a href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz">another</a> describes the package that automates their declaration.
-
-</body>
-</html>