--- 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} *}
--- 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%
%