# HG changeset patch
# User wenzelm
# Date 1343498841 -7200
# Node ID 8026c852cc10f00676783cecaf48d6012e1b5e67
# Parent  ed975dbb16ca8686a609b88fb8cda69b8a5b4cfc
some introduction on sessions;

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} *}
 
diff -r ed975dbb16ca -r 8026c852cc10 doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Sat Jul 28 19:49:09 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Sat Jul 28 20:07:21 2012 +0200
@@ -18,12 +18,31 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Isabelle sessions and build management%
+\isamarkupchapter{Isabelle sessions and build management \label{ch:session}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+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.
+
+  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 \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}, which itself is based on \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} 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.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %