diff -r c143ad7811fc -r da1fdbfebd39 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Tue Jul 30 12:07:14 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Tue Jul 30 15:09:25 2013 +0200
@@ -22,13 +22,7 @@
 
   \medskip The toplevel maintains an implicit state, which is
   transformed by a sequence of transitions -- either interactively or
-  in batch-mode.  In interactive mode, Isar state transitions are
-  encapsulated as safe transactions, such that both failure and undo
-  are handled conveniently without destroying the underlying draft
-  theory (cf.~\secref{sec:context-theory}).  In batch mode,
-  transitions operate in a linear (destructive) fashion, such that
-  error conditions abort the present attempt to construct a theory or
-  proof altogether.
+  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