# HG changeset patch
# User wenzelm
# Date 1403173984 -7200
# Node ID e0f573aca42f9928681c499550e9d017fc78a323
# Parent  1dc320dc2ada1a30b07b6ce2c47278f53706a7a5
tuned;

diff -r 1dc320dc2ada -r e0f573aca42f src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Thu Jun 19 12:05:10 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy	Thu Jun 19 12:33:04 2014 +0200
@@ -8,43 +8,30 @@
 
 section {* Isar toplevel \label{sec:isar-toplevel} *}
 
-text {* The Isar toplevel may be considered the central hub of the
-  Isabelle/Isar system, where all key components and sub-systems are
-  integrated into a single read-eval-print loop of Isar commands,
-  which also incorporates the underlying ML compiler.
+text {*
+  The Isar \emph{toplevel state} represents the outermost configuration that
+  is transformed by a sequence of transitions (commands) within a theory body.
+  This is a pure value with pure functions acting on it in a timeless and
+  stateless manner. Historically, the sequence of transitions was wrapped up
+  as sequential command loop, such that commands are applied sequentially
+  one-by-one. In contemporary Isabelle/Isar, processing toplevel commands
+  usually works in parallel in multi-threaded Isabelle/ML.
+*}
 
-  Isabelle/Isar departs from the original ``LCF system architecture''
-  where ML was really The Meta Language for defining theories and
-  conducting proofs.  Instead, ML now only serves as the
-  implementation language for the system (and user extensions), while
-  the specific Isar toplevel supports the concepts of theory and proof
-  development natively.  This includes the graph structure of theories
-  and the block structure of proofs, support for unlimited undo,
-  facilities for tracing, debugging, timing, profiling etc.
-
-  \medskip The toplevel maintains an implicit state, which is
-  transformed by a sequence of transitions -- either interactively or
-  in batch-mode.
 
-  The toplevel state is a disjoint sum of empty @{text toplevel}, or
-  @{text theory}, or @{text proof}.  On entering the main Isar loop we
-  start with an empty toplevel.  A theory is commenced by giving a
-  @{text \<THEORY>} header; within a theory we may issue theory
-  commands such as @{text \<DEFINITION>}, or state a @{text
-  \<THEOREM>} to be proven.  Now we are within a proof state, with a
-  rich collection of Isar proof commands for structured proof
-  composition, or unstructured proof scripts.  When the proof is
-  concluded we get back to the theory, which is then updated by
-  storing the resulting fact.  Further theory declarations or theorem
-  statements with proofs may follow, until we eventually conclude the
-  theory development by issuing @{text \<END>}.  The resulting theory
-  is then stored within the theory database and we are back to the
-  empty toplevel.
+subsection {* Toplevel state *}
 
-  In addition to these proper state transformations, there are also
-  some diagnostic commands for peeking at the toplevel state without
-  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
-  \isakeyword{print-cases}).
+text {*
+  The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text
+  theory}, or @{text proof}. The initial toplevel is empty; a theory is
+  commenced by a @{command theory} header; within a theory we may use theory
+  commands such as @{command definition}, or state a @{command theorem} to be
+  proven. A proof state accepts a rich collection of Isar proof commands for
+  structured proof composition, or unstructured proof scripts. When the proof
+  is concluded we get back to the theory, which is then updated by defining
+  the resulting fact. Further theory declarations or theorem statements with
+  proofs may follow, until we eventually conclude the theory development by
+  issuing @{command end} to get back to the empty toplevel.
 *}
 
 text %mlref {*
@@ -62,9 +49,7 @@
 
   \item Type @{ML_type Toplevel.state} represents Isar toplevel
   states, which are normally manipulated through the concept of
-  toplevel transitions only (\secref{sec:toplevel-transition}).  Also
-  note that a raw toplevel state is subject to the same linearity
-  restrictions as a theory context (cf.~\secref{sec:context-theory}).
+  toplevel transitions only (\secref{sec:toplevel-transition}).
 
   \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
   operations.  Many operations work only partially for certain cases,