diff -r ed975dbb16ca -r 8026c852cc10 doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Sat Jul 28 19:49:09 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Sat Jul 28 20:07:21 2012 +0200
@@ -2,9 +2,30 @@
 imports Base
 begin
 
-chapter {* Isabelle sessions and build management *}
+chapter {* Isabelle sessions and build management \label{ch:session} *}
+
+text {* An Isabelle \emph{session} consists of a collection of related
+  theories that are associated with an optional formal document (see
+  also \chref{ch:present}).  There is also a notion of persistent
+  \emph{heap image} to capture the state of a session, similar to
+  object-code in compiled programming languages.
 
-text {* FIXME *}
+  Thus the concept of session resembles that of a ``project'' in
+  common IDE environments, but our specific name emphasizes the
+  connection to interactive theorem proving: the session wraps-up the
+  results of user-interaction with the prover in a persistent form.
+
+  \medskip Application sessions are built on a given parent session.
+  The resulting hierarchy eventually leads to some major object-logic
+  session, notably @{text "HOL"}, which itself is based on @{text
+  "Pure"} as the common root.
+
+  Processing sessions may take considerable time.  The tools for
+  Isabelle build management help to organize this efficiently,
+  including support for parallel build jobs --- in addition to the
+  multithreaded theory and proof checking that is already provided by
+  the prover process.
+*}
 
 section {* Session ROOT specifications \label{sec:session-root} *}