--- a/doc-src/IsarImplementation/Thy/document/integration.tex Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Mon Sep 04 20:07:55 2006 +0200
@@ -150,10 +150,10 @@
The operational part is represented as the sequential union of a
list of partial functions, which are tried in turn until the first
- one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|). This acts
- like an outer case-expression for various alternative state
- transitions. For example, \isakeyword{qed} acts differently for a
- local proofs vs.\ the global ending of the main proof.
+ one succeeds. This acts like an outer case-expression for various
+ alternative state transitions. For example, \isakeyword{qed} acts
+ differently for a local proofs vs.\ the global ending of the main
+ proof.
Toplevel transitions are composed via transition transformers.
Internally, Isar commands are put together from an empty transition
@@ -274,9 +274,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The {\ML} toplevel provides a read-compile-eval-print loop for
- {\ML} values, types, structures, and functors. {\ML} declarations
- operate on the global system state, which consists of the compiler
+The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
+ values, types, structures, and functors. {\ML} declarations operate
+ on the global system state, which consists of the compiler
environment plus the values of {\ML} reference variables. There is
no clean way to undo {\ML} declarations, except for reverting to a
previously saved state of the whole Isabelle process. {\ML} input