merged
authorwenzelm
Tue, 12 Mar 2013 22:24:01 +0100
changeset 51405 2aea76fe9c73
parent 51396 f4c82c165f58 (current diff)
parent 51404 90a598019aeb (diff)
child 51406 950b897f95bb
merged
src/CTT/README.html
src/Cube/README.html
src/FOL/README.html
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/LCF/README.html
src/Sequents/README.html
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/Resid/README.html
src/ZF/ex/README.html
--- a/NEWS	Tue Mar 12 19:55:17 2013 +0100
+++ b/NEWS	Tue Mar 12 22:24:01 2013 +0100
@@ -61,6 +61,14 @@
       isar_shrink ~> isar_compress
 
 
+*** System ***
+
+* Discontinued "isabelle usedir" option -P (remote path) and -r (reset
+session path).  Note that usedir is legacy and superseded by "isabelle
+build" since Isabelle2013.
+
+
+
 New in Isabelle2013 (February 2013)
 -----------------------------------
 
--- a/src/CCL/ROOT	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/CCL/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,3 +1,5 @@
+chapter CCL
+
 session CCL = Pure +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
--- a/src/CTT/README.html	Tue Mar 12 19:55:17 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 19:55:17 2013 +0100
+++ b/src/CTT/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,20 @@
+chapter CTT
+
 session CTT = Pure +
   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 19:55:17 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 19:55:17 2013 +0100
+++ b/src/Cube/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,9 +1,17 @@
+chapter Cube
+
 session Cube = Pure +
   description {*
     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/Doc/ROOT	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Doc/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,3 +1,5 @@
+chapter Doc
+
 session Classes (doc) in "Classes" = HOL +
   options [document_variants = "classes"]
   theories [document = false] Setup
--- a/src/FOL/README.html	Tue Mar 12 19:55:17 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 19:55:17 2013 +0100
+++ b/src/FOL/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,10 +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/FOLP/ROOT	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/FOLP/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,3 +1,5 @@
+chapter FOLP
+
 session FOLP = Pure +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
--- a/src/HOL/Algebra/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/Algebra/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -110,9 +110,6 @@
 <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
   Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.
 
-<HR>
-<P>Last modified on $Date$
-
 <ADDRESS>
 <P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
 </ADDRESS>
--- a/src/HOL/Auth/Guard/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/Auth/Guard/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
--- a/src/HOL/Auth/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/Auth/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
@@ -46,9 +44,6 @@
 <P>Frederic Blanqui has contributed a theory of guardedness, which is
 demonstrated by proofs of some roving agent protocols.
 
-<HR>
-<P>Last modified $Date$
-
 <ADDRESS>
 <A
 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
--- a/src/HOL/HOLCF/FOCUS/README.html	Tue Mar 12 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 2013 +0100
+++ b/src/HOL/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,3 +1,5 @@
+chapter HOL
+
 session HOL (main) = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
@@ -48,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
@@ -115,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
@@ -129,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"
@@ -145,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"
@@ -215,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
@@ -229,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
@@ -313,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"
@@ -326,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
@@ -344,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"
@@ -359,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},
@@ -483,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"
@@ -509,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
 
@@ -635,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"
@@ -862,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"
@@ -883,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
@@ -892,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/HOL/TLA/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/TLA/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
--- a/src/HOL/UNITY/Comp/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/UNITY/Comp/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
@@ -40,9 +38,6 @@
 level of automation appears to be about the same as in HOL-UNITY by Flemming
 Andersen et al.
 
-<HR>
-<P>Last modified on $Date$
-
 <ADDRESS>
 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
 </ADDRESS>
--- a/src/HOL/UNITY/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/UNITY/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
@@ -45,9 +43,6 @@
 The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
 presents examples of proofs involving program composition.
 
-<HR>
-<P>Last modified on $Date$
-
 <ADDRESS>
 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
 </ADDRESS>
--- a/src/HOL/UNITY/Simple/README.html	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/HOL/UNITY/Simple/README.html	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
@@ -37,9 +35,6 @@
 <A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
 </UL>
 
-<HR>
-<P>Last modified on $Date$
-
 <ADDRESS>
 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
 </ADDRESS>
--- a/src/LCF/README.html	Tue Mar 12 19:55:17 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 19:55:17 2013 +0100
+++ b/src/LCF/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,7 +1,14 @@
+chapter LCF
+
 session LCF = Pure +
   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/Pure/ROOT	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,3 +1,5 @@
+chapter Pure
+
 session RAW =
   theories
   files
--- a/src/Pure/System/session.ML	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/System/session.ML	Tue Mar 12 22:24:01 2013 +0100
@@ -1,18 +1,16 @@
 (*  Title:      Pure/System/session.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Session management -- maintain state of logic images.
+Session management -- internal state of logic images.
 *)
 
 signature SESSION =
 sig
-  val id: unit -> string list
   val name: unit -> string
-  val path: unit -> string list
   val welcome: unit -> string
+  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+    string -> string * string -> bool * string -> bool -> unit
   val finish: unit -> unit
-  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string -> string -> bool * string -> string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
@@ -24,22 +22,10 @@
 
 (* session state *)
 
-val session = Unsynchronized.ref ([Context.PureN]: string list);
+val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
 val session_finished = Unsynchronized.ref false;
 
-fun id () = ! session;
-fun name () = "Isabelle/" ^ List.last (! session);
-
-
-(* access path *)
-
-val session_path = Unsynchronized.ref ([]: string list);
-val remote_path = Unsynchronized.ref (NONE: Url.T option);
-
-fun path () = ! session_path;
-
-
-(* welcome *)
+fun name () = "Isabelle/" ^ #name (! session);
 
 fun welcome () =
   if Distribution.is_official then
@@ -47,22 +33,21 @@
   else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
 
 
-(* add_path *)
+(* init *)
 
-fun add_path reset s =
-  let val sess = ! session @ [s] in
-    (case duplicates (op =) sess of
-      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
-    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
-  end;
-
-
-(* init_name *)
-
-fun init_name reset parent name =
-  if not (member (op =) (! session) parent) orelse not (! session_finished) then
+fun init build info info_path doc doc_graph doc_output doc_variants
+    parent (chapter, name) doc_dump verbose =
+  if #name (! session) <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
-  else (add_path reset name; session_finished := false);
+  else
+    let
+      val _ = session := {chapter = chapter, name = name};
+      val _ = session_finished := false;
+    in
+      Present.init build info info_path (if doc = "false" then "" else doc)
+        doc_graph doc_output doc_variants (chapter, name)
+        doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
+    end;
 
 
 (* finish *)
@@ -78,7 +63,7 @@
   session_finished := true);
 
 
-(* use_dir *)
+(* timing within ML *)
 
 fun with_timing name verbose f x =
   let
@@ -100,29 +85,13 @@
       else ();
   in y end;
 
-fun get_rpath rpath =
-  (if rpath = "" then () else
-     if is_some (! remote_path) then
-       error "Path for remote theory browsing information may only be set once"
-     else
-       remote_path := SOME (Url.explode rpath);
-   (! remote_path, rpath <> ""));
 
-fun init build reset info info_path doc doc_graph doc_output doc_variants
-    parent name doc_dump rpath verbose =
- (init_name reset parent name;
-  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
-    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
-    (map Thy_Info.get_theory (Thy_Info.get_names ())));
-
-local
+(* use_dir *)
 
 fun read_variants strs =
   rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   |> filter_out (fn (_, s) => s = "-");
 
-in
-
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name doc_dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
@@ -132,8 +101,15 @@
         Output.physical_stderr
           "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
       val _ =
-        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
-          doc_dump rpath verbose;
+        if not reset then ()
+        else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n";
+      val _ =
+        if rpath = "" then ()
+        else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
+
+      val _ =
+        init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants)
+          parent ("Unsorted", name) doc_dump verbose;
       val res1 = (use |> with_timing item timing |> Exn.capture) root;
       val res2 = Exn.capture finish ();
     in ignore (Par_Exn.release_all [res1, res2]) end)
@@ -148,5 +124,3 @@
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
 
 end;
-
-end;
--- a/src/Pure/Thy/html.ML	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Thy/html.ML	Tue Mar 12 22:24:01 2013 +0100
@@ -22,12 +22,11 @@
   val verbatim: string -> text
   val begin_document: string -> text
   val end_document: text
-  val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
+  val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
   val applet_pages: string -> Url.T * string -> (string * string) list
   val theory_entry: Url.T * string -> text
-  val session_entries: (Url.T * string) list -> text
   val theory_source: text -> text
-  val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
+  val begin_theory: string -> (Url.T option * string) list ->
     (Url.T * Url.T * bool) list -> text -> text
   val external_file: Url.T -> string -> text
 end;
@@ -288,15 +287,11 @@
 
 val end_document = "\n</div>\n</body>\n</html>\n";
 
-fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
-val up_link = gen_link "Up";
-val back_link = gen_link "Back";
-
 
 (* session index *)
 
-fun begin_index up (index_path, session) docs graph =
-  begin_document ("Index of " ^ session) ^ up_link up ^
+fun begin_session_index session docs graph =
+  begin_document ("Session " ^ plain session) ^
   para ("View " ^ href_path graph "theory dependencies" ^
     implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
   "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
@@ -304,6 +299,8 @@
 fun choice chs s = space_implode " " (map (fn (s', lnk) =>
   enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
 
+fun back_link (path, name) = para (href_path path "Back" ^ " to index of " ^ plain name);
+
 fun applet_pages session back =
   let
     val sizes =
@@ -329,14 +326,7 @@
   in map applet_page sizes end;
 
 
-fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
-
-val theory_entry = entry;
-
-fun session_entries [] = "</ul>"
-  | session_entries es =
-      "</ul>\n</div>\n<div class=\"sessions\">\n\
-      \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
+fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
 
 
 (* theory *)
@@ -350,9 +340,8 @@
   fun file (href, path, loadit) =
     href_path href (if loadit then file_path path else enclose "(" ")" (file_path path));
 
-  fun theory up A =
-    begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
-    command "theory" ^ " " ^ name A;
+  fun theory A =
+    begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A;
 
   fun imports Bs =
     keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
@@ -360,8 +349,8 @@
   fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n";
 in
 
-fun begin_theory up A Bs Ps body =
-  theory up A ^ "<br/>\n" ^
+fun begin_theory A Bs Ps body =
+  theory A ^ "<br/>\n" ^
   imports Bs ^ "<br/>\n" ^
   (if null Ps then "" else uses Ps) ^
   body;
--- a/src/Pure/Thy/html.scala	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Thy/html.scala	Tue Mar 12 22:24:01 2013 +0100
@@ -11,7 +11,7 @@
 
 object HTML
 {
-  // encode text
+  /* encode text */
 
   def encode(text: String): String =
   {
@@ -29,19 +29,45 @@
   }
 
 
-  // common markup elements
+  /* document */
+
+  val end_document = "\n</div>\n</body>\n</html>\n"
 
-  def session_entry(name: String): String =
+  def begin_document(title: String): String =
+    "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
+    "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
+    "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
+    "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
+    "<head>\n" +
+    "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
+    "<title>" + encode(title) + "</title>\n" +
+    "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
+    "</head>\n" +
+    "\n" +
+    "<body>\n" +
+    "<div class=\"head\">" +
+    "<h1>" + encode(title) + "</h1>\n"
+
+
+  /* common markup elements */
+
+  private def session_entry(entry: (String, String)): String =
+  {
+    val (name, description) = entry
+    val descr =
+      if (description == "") Nil
+      else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
     XML.string_of_tree(
       XML.elem("li",
         List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
-          List(XML.Text(name)))))) + "\n"
+          List(XML.Text(name)))) ::: descr)) + "\n"
+  }
 
-  def session_entries(names: List[String]): String =
-    if (names.isEmpty) "</ul>"
-    else
-      "</ul>\n</div>\n<div class=\"sessions\">\n" +
-      "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
-
-  val end_document = "\n</div>\n</body>\n</html>\n"
+  def chapter_index(chapter: String, sessions: List[(String, String)]): String =
+  {
+    begin_document("Isabelle/" + chapter + " sessions") +
+      (if (sessions.isEmpty) ""
+       else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
+    end_document
+  }
 }
--- a/src/Pure/Thy/present.ML	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Thy/present.ML	Tue Mar 12 22:24:01 2013 +0100
@@ -14,9 +14,8 @@
   include BASIC_PRESENT
   val session_name: theory -> string
   val read_variant: string -> string * string
-  val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string list -> string -> bool * string -> Url.T option * bool -> bool ->
-    theory list -> unit  (*not thread-safe!*)
+  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+    string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit
   val theory_source: string -> (unit -> HTML.text) -> unit
@@ -45,15 +44,6 @@
 val graph_pdf_path = Path.basic "session_graph.pdf";
 val graph_eps_path = Path.basic "session_graph.eps";
 
-val session_path = Path.basic ".session";
-val session_entries_path = Path.explode ".session/entries";
-val pre_index_path = Path.explode ".session/pre-index";
-
-fun mk_rel_path [] ys = Path.make ys
-  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
-  | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
-      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
-
 fun show_path path = Path.implode (Path.append (File.pwd ()) path);
 
 
@@ -62,37 +52,48 @@
 
 structure Browser_Info = Theory_Data
 (
-  type T = {name: string, session: string list, is_local: bool};
-  val empty = {name = "", session = [], is_local = false}: T;
+  type T = {chapter: string, name: string};
+  val empty = {chapter = Context.PureN, name = Context.PureN}: T;
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
-val put_info = Browser_Info.put;
-val get_info = Browser_Info.get;
-val session_name = #name o get_info;
+val session_name = #name o Browser_Info.get;
+val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
 
 
 
 (** graphs **)
 
 fun ID_of sess s = space_implode "/" (sess @ [s]);
-fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
+fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy);
 
+fun theory_link (curr_chapter, curr_session) thy =
+  let
+    val {chapter, name = session} = Browser_Info.get thy;
+    val link = html_path (Context.theory_name thy);
+  in
+    if curr_session = session then SOME link
+    else if curr_chapter = chapter then
+      SOME (Path.appends [Path.parent, Path.basic session, link])
+    else if chapter = Context.PureN then NONE
+    else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
+  end;
 
 (*retrieve graph data from initial collection of theories*)
-fun init_graph remote_path curr_sess = rev o map (fn thy =>
+fun init_graph (curr_chapter, curr_session) = rev o map (fn thy =>
   let
-    val name = Context.theory_name thy;
-    val {name = sess_name, session, is_local} = get_info thy;
+    val {chapter, name = session_name} = Browser_Info.get thy;
+    val thy_name = Context.theory_name thy;
+    val path =
+      (case theory_link (curr_chapter, curr_session) thy of
+        NONE => ""
+      | SOME p => Path.implode p);
     val entry =
-     {name = name, ID = ID_of session name, dir = sess_name,
-      path =
-        if null session then "" else
-        if is_some remote_path andalso not is_local then
-          Url.implode (Url.append (the remote_path) (Url.File
-            (Path.append (Path.make session) (html_path name))))
-        else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
+     {name = thy_name,
+      ID = ID_of [chapter, session_name] thy_name,
+      dir = session_name,
+      path = path,
       unfold = false,
       parents = map ID_of_thy (Theory.parents_of thy),
       content = []};
@@ -130,8 +131,8 @@
 
 val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
 
-fun init_browser_info remote_path curr_sess thys = make_browser_info
-  (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
+fun init_browser_info session thys =
+  make_browser_info (Symtab.empty, [], [], [], init_graph session thys);
 
 fun map_browser_info f {theories, files, tex_index, html_index, graph} =
   make_browser_info (f (theories, files, tex_index, html_index, graph));
@@ -189,54 +190,30 @@
 (* session_info *)
 
 type session_info =
-  {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
+  {name: string, chapter: string, info_path: Path.T,
     info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
-    documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option,
-    verbose: bool, readme: Path.T option};
+    documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
+    readme: Path.T option};
 
 fun make_session_info
-  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
-    documents, doc_dump, remote_path, verbose, readme) =
-  {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
-    info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
-    documents = documents, doc_dump = doc_dump, remote_path = remote_path,
-    verbose = verbose, readme = readme}: session_info;
+  (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
+    documents, doc_dump, verbose, readme) =
+  {name = name, chapter = chapter, info_path = info_path, info = info,
+    doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
+    documents = documents, doc_dump = doc_dump, verbose = verbose,
+    readme = readme}: session_info;
 
 
 (* state *)
 
 val session_info = Unsynchronized.ref (NONE: session_info option);
 
-fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
+fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
 
 
 
 (** document preparation **)
 
-(* maintain session index *)
-
-val session_entries =
-  HTML.session_entries o
-    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
-
-fun get_entries dir =
-  split_lines (File.read (Path.append dir session_entries_path));
-
-fun put_entries entries dir =
-  File.write (Path.append dir session_entries_path) (cat_lines entries);
-
-
-fun create_index dir =
-  File.read (Path.append dir pre_index_path) ^
-    session_entries (get_entries dir) ^ HTML.end_document
-  |> File.write (Path.append dir index_path);
-
-fun update_index dir name =
-  (case try get_entries dir of
-    NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
-  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
-
-
 (* document variants *)
 
 fun read_variant str =
@@ -248,19 +225,14 @@
 
 (* init session *)
 
-fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
-
-fun init build info info_path doc doc_graph document_output doc_variants path name
-    (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys =
+fun init build info info_path doc doc_graph document_output doc_variants
+    (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys =
   if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
-      val parent_name = name_of_session (take (length path - 1) path);
-      val session_name = name_of_session path;
-      val sess_prefix = Path.make path;
-      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
-      val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
+      val doc_output =
+        if document_output = "" then NONE else SOME (Path.explode document_output);
 
       val documents =
         if doc = "" then []
@@ -269,11 +241,6 @@
            else (); [])
         else doc_variants;
 
-      val parent_index_path = Path.append Path.parent index_path;
-      val index_up_lnk =
-        if first_time then
-          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
-        else Url.File parent_index_path;
       val readme =
         if File.exists readme_html_path then SOME readme_html_path
         else if File.exists readme_path then SOME readme_path
@@ -282,14 +249,12 @@
       val docs =
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
           map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
-      val index_text = HTML.begin_index (index_up_lnk, parent_name)
-        (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
       session_info :=
-        SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
-          doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
-      browser_info := init_browser_info remote_path path thys;
-      add_html_index (0, index_text)
+        SOME (make_session_info (name, chapter, info_path, info, doc,
+          doc_graph, doc_output, documents, doc_dump, verbose, readme));
+      browser_info := init_browser_info (chapter, name) thys;
+      add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
     end;
 
 
@@ -337,15 +302,18 @@
 
 
 fun finish () =
-  session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
-    documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} =>
+  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
+    documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
   let
     val {theories, files, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
-    val parent_html_prefix = Path.append html_prefix Path.parent;
+
+    val chapter_prefix = Path.append info_path (Path.basic chapter);
+    val session_prefix = Path.append chapter_prefix (Path.basic name);
 
     fun finish_html (a, {html, ...}: theory_info) =
-      File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
+      File.write_buffer (Path.append session_prefix (html_path a))
+        (Buffer.add HTML.end_document html);
 
     val sorted_graph = sorted_index graph;
     val opt_graphs =
@@ -355,21 +323,19 @@
 
     val _ =
       if info then
-       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
-        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
-        File.write (Path.append html_prefix session_entries_path) "";
-        create_index html_prefix;
-        if length path > 1 then update_index parent_html_prefix name else ();
-        (case readme of NONE => () | SOME path => File.copy path html_prefix);
-        Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph;
+       (Isabelle_System.mkdirs session_prefix;
+        File.write_buffer (Path.append session_prefix index_path)
+          (index_buffer html_index |> Buffer.add HTML.end_document);
+        (case readme of NONE => () | SOME path => File.copy path session_prefix);
+        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
         Isabelle_System.isabelle_tool "browser" "-b";
-        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
-        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
+        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
+        List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
           (HTML.applet_pages name (Url.File index_path, name));
-        File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
+        File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
         List.app finish_html thys;
         List.app (uncurry File.write) files;
-        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+        if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
         else ())
       else ();
 
@@ -415,7 +381,7 @@
 
     val jobs =
       (if info orelse is_none doc_output then
-        map (document_job html_prefix true) documents
+        map (document_job session_prefix true) documents
        else []) @
       (case doc_output of
         NONE => []
@@ -430,33 +396,23 @@
 
 (* theory elements *)
 
-fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
+fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info);
 
 fun theory_source name mk_text =
-  session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
+  with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
 
 fun theory_output name s =
-  session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
+  with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
 
 
-fun parent_link remote_path curr_session thy =
-  let
-    val {name = _, session, is_local} = get_info thy;
-    val name = Context.theory_name thy;
-    val link =
-      if null session then NONE
-      else SOME
-       (if is_some remote_path andalso not is_local then
-         Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))
-        else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
-  in (link, name) end;
-
 fun begin_theory update_time dir thy =
-    session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
+    with_session_info thy (fn {name = session_name, chapter, info_path, ...} =>
   let
     val name = Context.theory_name thy;
     val parents = Theory.parents_of thy;
-    val parent_specs = map (parent_link remote_path path) parents;
+    val parent_specs = parents |> map (fn parent =>
+      (Option.map Url.File (theory_link (chapter, session_name) parent),
+        (Context.theory_name parent)));
 
     val files = [];  (* FIXME *)
     val files_html = files |> map (fn (raw_path, loadit) =>
@@ -464,18 +420,22 @@
         val path = File.check_file (File.full_path dir raw_path);
         val base = Path.base path;
         val base_html = html_ext base;
-        val _ = add_file (Path.append html_prefix base_html,
-          HTML.external_file (Url.File base) (File.read path));
+        (* FIXME retain file path!? *)
+        val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name];
+        val _ =
+          add_file (Path.append session_prefix base_html,
+            HTML.external_file (Url.File base) (File.read path));
       in (Url.File base_html, Url.File raw_path, loadit) end);
 
     fun prep_html_source (tex_source, html_source, html) =
-      let
-        val txt = HTML.begin_theory (Url.File index_path, session)
-          name parent_specs files_html (Buffer.content html_source)
+      let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source)
       in (tex_source, Buffer.empty, Buffer.add txt html) end;
 
     val entry =
-     {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
+     {name = name,
+      ID = ID_of [chapter, session_name] name,
+      dir = session_name,
+      unfold = true,
       path = Path.implode (html_path name),
       parents = map ID_of_thy parents,
       content = []};
@@ -484,7 +444,7 @@
     add_graph_entry (update_time, entry);
     add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
     add_tex_index (update_time, Latex.theory_entry name);
-    put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
+    Browser_Info.put {chapter = chapter, name = session_name} thy
   end);
 
 
--- a/src/Pure/Thy/present.scala	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Thy/present.scala	Tue Mar 12 22:24:01 2013 +0100
@@ -7,35 +7,41 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedMap
+
+
 object Present
 {
-  /* maintain session index -- NOT thread-safe */
+  /* maintain chapter index -- NOT thread-safe */
 
   private val index_path = Path.basic("index.html")
-  private val session_entries_path = Path.explode(".session/entries")
-  private val pre_index_path = Path.explode(".session/pre-index")
+  private val sessions_path = Path.basic(".sessions")
 
-  private def get_entries(dir: Path): List[String] =
-    split_lines(File.read(dir + session_entries_path))
+  private def read_sessions(dir: Path): List[(String, String)] =
+  {
+    import XML.Decode._
+    list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path)))
+  }
 
-  private def put_entries(entries: List[String], dir: Path): Unit =
-    File.write(dir + session_entries_path, cat_lines(entries))
+  private def write_sessions(dir: Path, sessions: List[(String, String)])
+  {
+    import XML.Encode._
+    File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
+  }
 
-  def create_index(dir: Path): Unit =
-    File.write(dir + index_path,
-      File.read(dir + pre_index_path) +
-      HTML.session_entries(get_entries(dir)) +
-      HTML.end_document)
+  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
+  {
+    val dir = info_path + Path.basic(chapter)
+    Isabelle_System.mkdirs(dir)
 
-  def update_index(dir: Path, names: List[String]): Unit =
-    try {
-      put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir)
-      create_index(dir)
-    }
-    catch {
-      case ERROR(msg) =>
-        java.lang.System.err.println(
-          "### " + msg + "\n### Browser info: failed to update session index of " + dir)
-    }
+    val sessions0 =
+      try { read_sessions(dir + sessions_path) }
+      catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
+
+    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
+
+    write_sessions(dir, sessions)
+    File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
+  }
 }
 
--- a/src/Pure/Tools/build.ML	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Tools/build.ML	Tue Mar 12 22:24:01 2013 +0100
@@ -109,11 +109,12 @@
 fun build args_file = Command_Line.tool (fn () =>
     let
       val (command_timings, (do_output, (options, (verbose, (browser_info,
-          (parent_name, (name, theories))))))) =
+          (parent_name, (chapter, (name, theories)))))))) =
         File.read (Path.explode args_file) |> YXML.parse_body |>
           let open XML.Decode in
             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
-              (pair string (pair string ((list (pair Options.decode (list string))))))))))
+              (pair string (pair string (pair string
+                ((list (pair Options.decode (list string)))))))))))
           end;
 
       val document_variants =
@@ -125,18 +126,15 @@
 
       val _ = writeln ("\fSession.name = " ^ name);
       val _ =
-        (case Session.path () of
-          [] => ()
-        | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
-      val _ =
-        Session.init do_output false
-          (Options.bool options "browser_info") browser_info
+        Session.init do_output
+          (Options.bool options "browser_info")
+          (Path.explode browser_info)
           (Options.string options "document")
           (Options.bool options "document_graph")
           (Options.string options "document_output")
           document_variants
-          parent_name name
-          (false, "") ""
+          parent_name (chapter, name)
+          (false, "")
           verbose;
 
       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
--- a/src/Pure/Tools/build.scala	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 12 22:24:01 2013 +0100
@@ -14,6 +14,7 @@
 import java.util.zip.GZIPInputStream
 
 import scala.collection.SortedSet
+import scala.collection.mutable
 import scala.annotation.tailrec
 
 
@@ -46,6 +47,8 @@
   /** session information **/
 
   // external version
+  abstract class Entry
+  sealed case class Chapter(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
     name: String,
@@ -55,10 +58,11 @@
     description: String,
     options: List[Options.Spec],
     theories: List[(List[Options.Spec], List[String])],
-    files: List[String])
+    files: List[String]) extends Entry
 
   // internal version
   sealed case class Session_Info(
+    chapter: String,
     select: Boolean,
     pos: Position.T,
     groups: List[String],
@@ -72,8 +76,8 @@
 
   def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
 
-  def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
-      : (String, Session_Info) =
+  def session_info(options: Options, select: Boolean, dir: Path,
+      chapter: String, entry: Session_Entry): (String, Session_Info) =
     try {
       val name = entry.name
 
@@ -87,10 +91,11 @@
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts, thys.map(Path.explode(_))) })
       val files = entry.files.map(Path.explode(_))
-      val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
+      val entry_digest =
+        SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString)
 
       val info =
-        Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+        Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
           entry.parent, entry.description, session_options, theories, files, entry_digest)
 
       (name, info)
@@ -180,6 +185,9 @@
 
   /* parser */
 
+  val chapter_default = "Unsorted"
+
+  private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
@@ -189,10 +197,20 @@
 
   lazy val root_syntax =
     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
+      IN + DESCRIPTION + OPTIONS + THEORIES + FILES
 
   private object Parser extends Parse.Parser
   {
+    def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
+
+    def chapter(pos: Position.T): Parser[Chapter] =
+    {
+      val chapter_name = atom("chapter name", _.is_name)
+
+      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
+    }
+
     def session_entry(pos: Position.T): Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
@@ -219,11 +237,19 @@
             Session_Entry(pos, a, b, c, d, e, f, g, h) }
     }
 
-    def parse_entries(root: Path): List[Session_Entry] =
+    def parse_entries(root: Path): List[(String, Session_Entry)] =
     {
       val toks = root_syntax.scan(File.read(root))
-      parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
-        case Success(result, _) => result
+
+      parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
+        case Success(result, _) =>
+          var chapter = chapter_default
+          val entries = new mutable.ListBuffer[(String, Session_Entry)]
+          result.foreach {
+            case Chapter(name) => chapter = name
+            case session_entry: Session_Entry => entries += ((chapter, session_entry))
+          }
+          entries.toList
         case bad => error(bad.toString)
       }
     }
@@ -250,7 +276,8 @@
     def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
     {
       val root = dir + ROOT
-      if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
+      if (root.is_file)
+        Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2))
       else Nil
     }
 
@@ -398,7 +425,7 @@
             val groups =
               if (info.groups.isEmpty) ""
               else info.groups.mkString(" (", " ", ")")
-            progress.echo("Session " + name + groups)
+            progress.echo("Session " + info.chapter + "/" + name + groups)
           }
 
           val thy_deps =
@@ -470,9 +497,10 @@
         {
           import XML.Encode._
               pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
-                pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+                pair(string, pair(string, pair(string,
+                  list(pair(Options.encode, list(Path.encode)))))))))))(
               (command_timings, (do_output, (info.options, (verbose, (browser_info,
-                (parent, (name, info.theories))))))))
+                (parent, (info.chapter, (name, info.theories)))))))))
         }))
 
     private val env =
@@ -568,7 +596,6 @@
   private def log_gz(name: String): Path = log(name).ext("gz")
 
   private val SESSION_NAME = "\fSession.name = "
-  private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
 
   sealed case class Log_Info(
@@ -727,7 +754,7 @@
     }
 
     // scheduler loop
-    case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
+    case class Result(current: Boolean, heap: String, rc: Int)
 
     def sleep(): Unit = Thread.sleep(500)
 
@@ -748,7 +775,7 @@
             val res = job.join
             progress.echo(res.err)
 
-            val (parent_path, heap) =
+            val heap =
               if (res.rc == 0) {
                 (output_dir + log(name)).file.delete
 
@@ -757,13 +784,7 @@
                 File.write_gzip(output_dir + log_gz(name),
                   sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
 
-                val parent_path =
-                  if (job.info.options.bool("browser_info"))
-                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH))
-                      .map(_.substring(SESSION_PARENT_PATH.length))
-                  else None
-
-                (parent_path, heap)
+                heap
               }
               else {
                 (output_dir + Path.basic(name)).file.delete
@@ -778,10 +799,10 @@
                   progress.echo("\n" + cat_lines(tail))
                 }
 
-                (None, no_heap)
+                no_heap
               }
             loop(pending - name, running - name,
-              results + (name -> Result(false, parent_path, heap, res.rc)))
+              results + (name -> Result(false, heap, res.rc)))
             //}}}
           case None if (running.size < (max_jobs max 1)) =>
             //{{{ check/start next job
@@ -789,7 +810,7 @@
               case Some((name, info)) =>
                 val parent_result =
                   info.parent match {
-                    case None => Result(true, None, no_heap, 0)
+                    case None => Result(true, no_heap, 0)
                     case Some(parent) => results(parent)
                   }
                 val output = output_dir + Path.basic(name)
@@ -812,10 +833,10 @@
                 val all_current = current && parent_result.current
 
                 if (all_current)
-                  loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
+                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
                 else if (no_build) {
                   if (verbose) progress.echo("Skipping " + name + " ...")
-                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
+                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
                 }
                 else if (parent_result.rc == 0 && !progress.stopped) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
@@ -826,7 +847,7 @@
                 }
                 else {
                   progress.echo(name + " CANCELLED")
-                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
+                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
@@ -847,11 +868,11 @@
       else loop(queue, Map.empty, Map.empty)
 
     val session_entries =
-      (for ((name, res) <- results.iterator if res.parent_path.isDefined)
-        yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
-          { case (p, es) => (p, es.map(_._2).sorted) })
-    for ((p, names) <- session_entries)
-      Present.update_index(browser_info + Path.explode(p), names)
+      (for { (name, res) <- results.iterator; info = full_tree(name) }
+        yield (info.chapter, (name, info.description))).toList.groupBy(_._1).map(
+          { case (chapter, es) => (chapter, es.map(_._2)) })
+    for ((chapter, entries) <- session_entries)
+      Present.update_chapter_index(browser_info, chapter, entries)
 
     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
     if (rc != 0 && (verbose || !no_build)) {
--- a/src/Sequents/README.html	Tue Mar 12 19:55:17 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 19:55:17 2013 +0100
+++ b/src/Sequents/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,9 +1,41 @@
+chapter Sequents
+
 session Sequents = Pure +
   description {*
     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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 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 19:55:17 2013 +0100
+++ b/src/ZF/ROOT	Tue Mar 12 22:24:01 2013 +0100
@@ -1,11 +1,46 @@
+chapter ZF
+
 session ZF (main) = Pure +
   description {*
     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
@@ -19,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
@@ -41,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,
@@ -49,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"
@@ -120,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
@@ -148,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 19:55:17 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 19:55:17 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>